This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zfregcl

Description: The Axiom of Regularity with class variables. (Contributed by NM, 5-Aug-1994) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021) Avoid ax-10 and ax-12 . (Revised by TM, 31-Dec-2025)

Ref Expression
Assertion zfregcl ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ ( 𝑧 = 𝐴 → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝐴 ) )
2 1 exbidv ⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑥 𝑥 ∈ 𝑧 ↔ ∃ 𝑥 𝑥 ∈ 𝐴 ) )
3 eleq2 ⊢ ( 𝑧 = 𝐴 → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝐴 ) )
4 3 notbid ⊢ ( 𝑧 = 𝐴 → ( ¬ 𝑦 ∈ 𝑧 ↔ ¬ 𝑦 ∈ 𝐴 ) )
5 4 ralbidv ⊢ ( 𝑧 = 𝐴 → ( ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧 ↔ ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴 ) )
6 5 rexeqbi1dv ⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴 ) )
7 2 6 imbi12d ⊢ ( 𝑧 = 𝐴 → ( ( ∃ 𝑥 𝑥 ∈ 𝑧 → ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧 ) ↔ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴 ) ) )
8 ax-reg ⊢ ( ∃ 𝑥 𝑥 ∈ 𝑧 → ∃ 𝑥 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧 ) ) )
9 df-ral ⊢ ( ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧 ) )
10 9 rexbii ⊢ ( ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧 ) )
11 df-rex ⊢ ( ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧 ) ) )
12 10 11 bitr2i ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧 ) ) ↔ ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧 )
13 8 12 sylib ⊢ ( ∃ 𝑥 𝑥 ∈ 𝑧 → ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧 )
14 7 13 vtoclg ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴 ) )