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

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 ⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )
cleqh.2 ⊢ ( 𝑦 ∈ 𝐵 → ∀ 𝑥 𝑦 ∈ 𝐵 )
Assertion cleqh ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 cleqh.1 ⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )
2 cleqh.2 ⊢ ( 𝑦 ∈ 𝐵 → ∀ 𝑥 𝑦 ∈ 𝐵 )
3 dfcleq ⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
4 nfv ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 )
5 1 nf5i ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
6 2 nf5i ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐵
7 5 6 nfbi ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 )
8 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
9 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
10 8 9 bibi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) ) )
11 4 7 10 cbvalv1 ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
12 3 11 bitr4i ⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )