Metamath Proof Explorer

Theorem cleqh

Description: Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions as in dfcleq . See also cleqf . (Contributed by NM, 26-May-1993) (Proof shortened by Wolf Lammen, 14-Nov-2019) Remove dependency on ax-13 . (Revised by BJ, 30-Nov-2020)

Ref Expression
Hypotheses cleqh.1 ⊢ y ∈ A → ∀ x y ∈ A
cleqh.2 ⊢ y ∈ B → ∀ x y ∈ B
Assertion cleqh ⊢ A = B ↔ ∀ x x ∈ A ↔ x ∈ B

Proof

Step Hyp Ref Expression
1 cleqh.1 ⊢ y ∈ A → ∀ x y ∈ A
2 cleqh.2 ⊢ y ∈ B → ∀ x y ∈ B
3 dfcleq ⊢ A = B ↔ ∀ y y ∈ A ↔ y ∈ B
4 nfv ⊢ Ⅎ y x ∈ A ↔ x ∈ B
5 1 nf5i ⊢ Ⅎ x y ∈ A
6 2 nf5i ⊢ Ⅎ 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