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

Proof

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