Quantorenregeln im Überblick

φ  ⇔ ∀x: φ ∀x:φ(x) ⇒ φ(a)
φ ⇔ ∃x:φ ∃x:φ(x) ⇐ φ(a)
∀z:φ(z) ⇒ ∀x∀y:φ(f(x,y,..)) ∃z:φ(z) ⇐ ∃x∃y:φ(f(x,y,..))
∀x:φ(x) ⇒ ∃x:φ(x)
∃x:φ(x)⇔¬∀x:¬φ(x)· ∀x:φ(x)⇔¬∃x:¬φ(x)·
¬∃x:φ(x)⇔∀x:¬φ(x)· ¬∀x:φ(x)⇔∃x:¬φ(x)·
 
(∀x:φ(x))∧a  ⇔ ∀x:φ(x)∧a (∃x:φ(x))∧a  ⇔ ∃x:φ(x)∧a ·
(∀x:φ(x))∨a  ⇔ ∀x:φ(x)∨a · (∃x:φ(x))∨a  ⇔ ∃x:φ(x)∨a
(∀x:φ(x))→a  ⇔ ∃x:φ(x)→a (∃x:φ(x))→a  ⇔ ∀x:φ(x)→a ·
(∀x:φ(x))←a  ⇔ ∀x:φ(x)←a · (∃x:φ(x))←a  ⇔ ∃x:φ(x)←a
 
∀x:∀y:φ(x,y) ⇔ ∀y:∀x:φ(x,y) · ∃x:∃y:φ(x,y) ⇔ ∃y:∃x:φ(x,y) ·
∃x:∀y:φ(x,y) ⇒ ∀y:∃x:φ(x,y) ·
 
∀z:φ(z)∧ψ(z) ⇔ ∀x:∀y:φ(x)∧ψ(y) · ∃z:φ(z)∨ψ(z) ⇔ ∃x:∃y:φ(x)∨ψ(y) ·
∀z:φ(z)∧ψ(z) ⇔ (∀x:φ(x)) ∧ (∀y:ψ(y)) · ∃z:φ(z)∨ψ(z) ⇔ (∃x:φ(x)) ∨ (∃y:ψ(y)) ·
∀z:φ(z)∨ψ(z) ⇐ (∀x:φ(x)) ∨ (∀y:ψ(y)) · ∃z:φ(z)∧ψ(z) ⇒ (∃x:φ(x)) ∧ (∃y:ψ(y)) ·
∀z:φ(z)→ψ(z) ⇐ (∃x:φ(x)) → (∀y:ψ(y)) · ∃z:φ(z)→ψ(z) ⇔ ∃x:∃y:φ(x)→ψ(y)·
∀z:φ(z)→ψ(z) ⇒ (∀x:φ(x)) → (∀y:ψ(y)) · ∃z:φ(z)→ψ(z) ⇔ (∀x:φ(x)) → (∃y:ψ(y)) ·
 
∀y:∃x:f(x)=y ⇒ (∀y:φ(y) ⇔ ∀x:φ(f(x))) ∀y:∃x:f(x)=y ⇒ (∃y:φ(y) ⇔ ∃x:φ(f(x)))
∀x:φ(f(x)) ⇔ ∀y:(∃x:f(x)=y)→φ(y) ∃x:φ(f(x)) ⇔∃y(∃x:f(x)=y)∧φ(y))
∀y:φ(y) ⇔ (∀x:φ(f(x))) ∧ (∀y:(∃x:f(x)=y)∨φ(y)) ∃y:φ(y) ⇔ (∀y:(φ(y)→∃x:f(x)=y) → ∃x:φ(f(x))
 
∀x:a(x)→b(x) ⇒ (∀x:a(x) ⇒ ∀x:b(x))· ∀x:a(x)↔b(x) ⇒ (∀x:φ(a(x)) ⇔ ∀x:φ(b(x)))·
∀x:a(x)→b(x) ⇒ (∃x:a(x) ⇒ ∃x:b(x))· ∀x:a(x)↔b(x) ⇒ (∃x:φ(a(x)) ⇔ ∃x:φ(b(x)))·
 
∀x∊A:φ(x)  =  ∀x:x∊A → φ(x) ∃x∊A:φ(x)  =  ∃x:x∊A ∧ φ(x)
A⊆B⇒ (∀x∊A:φ(x) ⇐ ∀x∊B:φ(x)) A⊆B⇒ (∃x∊A:φ(x) ⇒ ∃x∊B:φ(x))
(∀x∊A:φ(x)) ∧(∀x∊B:φ(x)) ⇔ ∀x∊A∪B:φ(x) (∃x∊A:φ(x)) ∨(∃x∊B:φ(x)) ⇔ ∃x∊A∪B:φ(x)
(∀x∊A:φ(x)) ∨(∀x∊B:φ(x)) ⇒ ∀x∊A∩B:φ(x) (∃x∊A:φ(x)) ∧(∃x∊B:φ(x)) ⇐ ∃x∊A∩B:φ(x)
∃x∊A:x=ψ  ⇔ ψ∊A ∃x:x=ψ ⇔ wahr

Bei bedingten Quantoren gelten alle Regeln dann, wenn die Trägermenge nicht leer ist. Die Regeln mit · gelten immer.