Metamath Proof Explorer


Theorem rabeqbidv

Description: Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009)

Ref Expression
Hypotheses rabeqbidv.1
|- ( ph -> A = B )
rabeqbidv.2
|- ( ph -> ( ps <-> ch ) )
Assertion rabeqbidv
|- ( ph -> { x e. A | ps } = { x e. B | ch } )

Proof

Step Hyp Ref Expression
1 rabeqbidv.1
 |-  ( ph -> A = B )
2 rabeqbidv.2
 |-  ( ph -> ( ps <-> ch ) )
3 2 adantr
 |-  ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
4 1 3 rabeqbidva
 |-  ( ph -> { x e. A | ps } = { x e. B | ch } )