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 ⊢ A ∈ V → ∃ x x ∈ A → ∃ x ∈ A ∀ y ∈ x ¬ y ∈ A

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ z = A → x ∈ z ↔ x ∈ A
2 1 exbidv ⊢ z = A → ∃ x x ∈ z ↔ ∃ x x ∈ A
3 eleq2 ⊢ z = A → y ∈ z ↔ y ∈ A
4 3 notbid ⊢ z = A → ¬ y ∈ z ↔ ¬ y ∈ A
5 4 ralbidv ⊢ z = A → ∀ y ∈ x ¬ y ∈ z ↔ ∀ y ∈ x ¬ y ∈ A
6 5 rexeqbi1dv ⊢ z = A → ∃ x ∈ z ∀ y ∈ x ¬ y ∈ z ↔ ∃ x ∈ A ∀ y ∈ x ¬ y ∈ A
7 2 6 imbi12d ⊢ z = A → ∃ x x ∈ z → ∃ x ∈ z ∀ y ∈ x ¬ y ∈ z ↔ ∃ x x ∈ A → ∃ x ∈ A ∀ y ∈ x ¬ y ∈ A
8 ax-reg ⊢ ∃ x x ∈ z → ∃ x x ∈ z ∧ ∀ y y ∈ x → ¬ y ∈ z
9 df-ral ⊢ ∀ y ∈ x ¬ y ∈ z ↔ ∀ y y ∈ x → ¬ y ∈ z
10 9 rexbii ⊢ ∃ x ∈ z ∀ y ∈ x ¬ y ∈ z ↔ ∃ x ∈ z ∀ y y ∈ x → ¬ y ∈ z
11 df-rex ⊢ ∃ x ∈ z ∀ y y ∈ x → ¬ y ∈ z ↔ ∃ x x ∈ z ∧ ∀ y y ∈ x → ¬ y ∈ z
12 10 11 bitr2i ⊢ ∃ x x ∈ z ∧ ∀ y y ∈ x → ¬ y ∈ z ↔ ∃ x ∈ z ∀ y ∈ x ¬ y ∈ z
13 8 12 sylib ⊢ ∃ x x ∈ z → ∃ x ∈ z ∀ y ∈ x ¬ y ∈ z
14 7 13 vtoclg ⊢ A ∈ V → ∃ x x ∈ A → ∃ x ∈ A ∀ y ∈ x ¬ y ∈ A