Metamath Proof Explorer

Theorem bj-rcleq

Description: Relative version of dfcleq . (Contributed by BJ, 27-Dec-2023)

Ref Expression
Assertion bj-rcleq 
|- ( ( V i^i A ) = ( V i^i B ) <-> A. x e. V ( x e. A <-> x e. B ) )

Proof

Step Hyp Ref Expression
1 nfcv 
 |-  F/_ x A
2 nfcv 
 |-  F/_ x B
3 nfcv 
 |-  F/_ x V
4 1 2 3 bj-rcleqf 
 |-  ( ( V i^i A ) = ( V i^i B ) <-> A. x e. V ( x e. A <-> x e. B ) )