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

Metamath Proof Explorer

Theorem cleqf

Description: Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions as in dfcleq . See also cleqh . (Contributed by NM, 26-May-1993) (Revised by Mario Carneiro, 7-Oct-2016) (Proof shortened by Wolf Lammen, 17-Nov-2019) Avoid ax-13 . (Revised by Wolf Lammen, 10-May-2023) Avoid ax-10 . (Revised by GG, 20-Aug-2023)

Ref Expression
Hypotheses cleqf.1 ⊢ Ⅎ _ x A
cleqf.2 ⊢ Ⅎ _ x B
Assertion cleqf ⊢ A = B ↔ ∀ x x ∈ A ↔ x ∈ B

Proof

Step Hyp Ref Expression
1 cleqf.1 ⊢ Ⅎ _ x A
2 cleqf.2 ⊢ Ⅎ _ x B
3 dfcleq ⊢ A = B ↔ ∀ y y ∈ A ↔ y ∈ B
4 nfv ⊢ Ⅎ y x ∈ A ↔ x ∈ B
5 1 nfcri ⊢ Ⅎ x y ∈ A
6 2 nfcri ⊢ Ⅎ x y ∈ B
7 5 6 nfbi ⊢ Ⅎ x y ∈ A ↔ y ∈ B
8 eleq1w ⊢ x = y → x ∈ A ↔ y ∈ A
9 eleq1w ⊢ x = y → x ∈ B ↔ y ∈ B
10 8 9 bibi12d ⊢ x = y → x ∈ A ↔ x ∈ B ↔ y ∈ A ↔ y ∈ B
11 4 7 10 cbvalv1 ⊢ ∀ x x ∈ A ↔ x ∈ B ↔ ∀ y y ∈ A ↔ y ∈ B
12 3 11 bitr4i ⊢ A = B ↔ ∀ x x ∈ A ↔ x ∈ B