Metamath Proof Explorer


Theorem bj-rabeqbid

Description: Version of rabeqbidv with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019)

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

Proof

Step Hyp Ref Expression
1 bj-rabeqbid.nf
 |-  F/ x ph
2 bj-rabeqbid.1
 |-  ( ph -> A = B )
3 bj-rabeqbid.2
 |-  ( ph -> ( ps <-> ch ) )
4 1 2 bj-rabeqd
 |-  ( ph -> { x e. A | ps } = { x e. B | ps } )
5 1 3 rabbid
 |-  ( ph -> { x e. B | ps } = { x e. B | ch } )
6 4 5 eqtrd
 |-  ( ph -> { x e. A | ps } = { x e. B | ch } )