Metamath Proof Explorer


Theorem bj-rabeqbida

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

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

Proof

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