Metamath Proof Explorer


Theorem bj-rabbida2

Description: Version of rabbidva2 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019)

Ref Expression
Hypotheses bj-rabbida2.nf
|- F/ x ph
bj-rabbida2.1
|- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) )
Assertion bj-rabbida2
|- ( ph -> { x e. A | ps } = { x e. B | ch } )

Proof

Step Hyp Ref Expression
1 bj-rabbida2.nf
 |-  F/ x ph
2 bj-rabbida2.1
 |-  ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) )
3 1 2 abbid
 |-  ( ph -> { x | ( x e. A /\ ps ) } = { x | ( x e. B /\ ch ) } )
4 df-rab
 |-  { x e. A | ps } = { x | ( x e. A /\ ps ) }
5 df-rab
 |-  { x e. B | ch } = { x | ( x e. B /\ ch ) }
6 3 4 5 3eqtr4g
 |-  ( ph -> { x e. A | ps } = { x e. B | ch } )