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 
|- ( y e. A -> A. x y e. A )
cleqh.2 
|- ( y e. B -> A. x y e. B )
Assertion cleqh 
|- ( A = B <-> A. x ( x e. A <-> x e. B ) )

Proof

Step Hyp Ref Expression
1 cleqh.1 
 |-  ( y e. A -> A. x y e. A )
2 cleqh.2 
 |-  ( y e. B -> A. x y e. B )
3 dfcleq 
 |-  ( A = B <-> A. y ( y e. A <-> y e. B ) )
4 nfv 
 |-  F/ y ( x e. A <-> x e. B )
5 1 nf5i 
 |-  F/ x y e. A
6 2 nf5i 
 |-  F/ x y e. B
7 5 6 nfbi 
 |-  F/ x ( y e. A <-> y e. B )
8 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
9 eleq1w 
 |-  ( x = y -> ( x e. B <-> y e. B ) )
10 8 9 bibi12d 
 |-  ( x = y -> ( ( x e. A <-> x e. B ) <-> ( y e. A <-> y e. B ) ) )
11 4 7 10 cbvalv1 
 |-  ( A. x ( x e. A <-> x e. B ) <-> A. y ( y e. A <-> y e. B ) )
12 3 11 bitr4i 
 |-  ( A = B <-> A. x ( x e. A <-> x e. B ) )