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 ( 𝑥 𝐴 → ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑦 𝑦 = 𝐴 ) )