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	⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )