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 ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴 ) )

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 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧
9 axreg2 ⊢ ( 𝑥 ∈ 𝑧 → ∃ 𝑥 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧 ) ) )
10 df-ral ⊢ ( ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧 ) )
11 10 rexbii ⊢ ( ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧 ) )
12 df-rex ⊢ ( ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧 ) ) )
13 11 12 bitr2i ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧 ) ) ↔ ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧 )
14 9 13 sylib ⊢ ( 𝑥 ∈ 𝑧 → ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧 )
15 8 14 exlimi ⊢ ( ∃ 𝑥 𝑥 ∈ 𝑧 → ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧 )
16 7 15 vtoclg ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴 ) )