Metamath Proof Explorer

Theorem bj-reabeq

Description: Relative form of abeq2 . (Contributed by BJ, 27-Dec-2023)

Ref Expression
Assertion bj-reabeq 
|- ( ( V i^i A ) = { x e. V | ph } <-> A. x e. V ( x e. A <-> ph ) )

Proof

Step Hyp Ref Expression
1 dfrab3 
 |-  { x e. V | ph } = ( V i^i { x | ph } )
2 1 eqeq2i 
 |-  ( ( V i^i A ) = { x e. V | ph } <-> ( V i^i A ) = ( V i^i { x | ph } ) )
3 nfcv 
 |-  F/_ x A
4 nfab1 
 |-  F/_ x { x | ph }
5 nfcv 
 |-  F/_ x V
6 3 4 5 bj-rcleqf 
 |-  ( ( V i^i A ) = ( V i^i { x | ph } ) <-> A. x e. V ( x e. A <-> x e. { x | ph } ) )
7 abid 
 |-  ( x e. { x | ph } <-> ph )
8 7 bibi2i 
 |-  ( ( x e. A <-> x e. { x | ph } ) <-> ( x e. A <-> ph ) )
9 8 ralbii 
 |-  ( A. x e. V ( x e. A <-> x e. { x | ph } ) <-> A. x e. V ( x e. A <-> ph ) )
10 2 6 9 3bitri 
 |-  ( ( V i^i A ) = { x e. V | ph } <-> A. x e. V ( x e. A <-> ph ) )