Description: Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep , we invoke the Axiom of Extensionality (indirectly via vtocl ), which is needed for the justification of class variable notation.
If we omit the requirement that y not occur in ph , we can derive a contradiction, as notzfaus shows. (Contributed by NM, 21-Jun-1993)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | zfauscl.1 | ⊢ 𝐴 ∈ V | |
| Assertion | zfauscl | ⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zfauscl.1 | ⊢ 𝐴 ∈ V | |
| 2 | eleq2 | ⊢ ( 𝑧 = 𝐴 → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝐴 ) ) | |
| 3 | 2 | anbi1d | ⊢ ( 𝑧 = 𝐴 → ( ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) |
| 4 | 3 | bibi2d | ⊢ ( 𝑧 = 𝐴 → ( ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) ) |
| 5 | 4 | albidv | ⊢ ( 𝑧 = 𝐴 → ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) ) |
| 6 | 5 | exbidv | ⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) ) |
| 7 | ax-sep | ⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) | |
| 8 | 1 6 7 | vtocl | ⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) |