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

Metamath Proof Explorer

Theorem zfregclOLD

Description: Obsolete version of zfregcl as of 31-Dec-2025. (Contributed by NM, 5-Aug-1994) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion zfregclOLD ⊢ 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 nfre1 ⊢ Ⅎ x ∃ x ∈ z ∀ y ∈ x ¬ y ∈ z
9 axreg2 ⊢ x ∈ z → ∃ x x ∈ z ∧ ∀ y y ∈ x → ¬ y ∈ z
10 df-ral ⊢ ∀ y ∈ x ¬ y ∈ z ↔ ∀ y y ∈ x → ¬ y ∈ z
11 10 rexbii ⊢ ∃ x ∈ z ∀ y ∈ x ¬ y ∈ z ↔ ∃ x ∈ z ∀ y y ∈ x → ¬ y ∈ z
12 df-rex ⊢ ∃ x ∈ z ∀ y y ∈ x → ¬ y ∈ z ↔ ∃ x x ∈ z ∧ ∀ y y ∈ x → ¬ y ∈ z
13 11 12 bitr2i ⊢ ∃ x x ∈ z ∧ ∀ y y ∈ x → ¬ y ∈ z ↔ ∃ x ∈ z ∀ y ∈ x ¬ y ∈ z
14 9 13 sylib ⊢ x ∈ z → ∃ x ∈ z ∀ y ∈ x ¬ y ∈ z
15 8 14 exlimi ⊢ ∃ x x ∈ z → ∃ x ∈ z ∀ y ∈ x ¬ y ∈ z
16 7 15 vtoclg ⊢ A ∈ V → ∃ x x ∈ A → ∃ x ∈ A ∀ y ∈ x ¬ y ∈ A