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 ⊢ Ⅎ _ x A → ∃ x x = A ↔ ∃ y y = A

Proof

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