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

Metamath Proof Explorer

Theorem cbvexeqsetf

Description: The expression E. x x = A means " A is a set" even if A contains x as a bound variable. This lemma helps minimizing axiom or df-clab usage in some cases. Extracted from the proof of issetft . (Contributed by Wolf Lammen, 30-Jul-2025)

Ref Expression
Assertion cbvexeqsetf ( Ⅎ 𝑥 𝐴 → ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑦 𝑦 = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 nfnfc1 ⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝐴
2 nfv ⊢ Ⅎ 𝑦 Ⅎ 𝑥 𝐴
3 nfvd ⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑦 ¬ 𝑥 = 𝐴 )
4 nfcvd ⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝑦 )
5 id ⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝐴 )
6 4 5 nfeqd ⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝑦 = 𝐴 )
7 6 nfnd ⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 ¬ 𝑦 = 𝐴 )
8 eqeq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝐴 ↔ 𝑦 = 𝐴 ) )
9 8 notbid ⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑥 = 𝐴 ↔ ¬ 𝑦 = 𝐴 ) )
10 9 a1i ⊢ ( Ⅎ 𝑥 𝐴 → ( 𝑥 = 𝑦 → ( ¬ 𝑥 = 𝐴 ↔ ¬ 𝑦 = 𝐴 ) ) )
11 1 2 3 7 10 cbv2w ⊢ ( Ⅎ 𝑥 𝐴 → ( ∀ 𝑥 ¬ 𝑥 = 𝐴 ↔ ∀ 𝑦 ¬ 𝑦 = 𝐴 ) )
12 alnex ⊢ ( ∀ 𝑥 ¬ 𝑥 = 𝐴 ↔ ¬ ∃ 𝑥 𝑥 = 𝐴 )
13 alnex ⊢ ( ∀ 𝑦 ¬ 𝑦 = 𝐴 ↔ ¬ ∃ 𝑦 𝑦 = 𝐴 )
14 11 12 13 3bitr3g ⊢ ( Ⅎ 𝑥 𝐴 → ( ¬ ∃ 𝑥 𝑥 = 𝐴 ↔ ¬ ∃ 𝑦 𝑦 = 𝐴 ) )
15 14 con4bid ⊢ ( Ⅎ 𝑥 𝐴 → ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑦 𝑦 = 𝐴 ) )