Theorem rabeqbidv 2730

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

Hypotheses

Ref	Expression
rabeqbidv.1	|- ( ph -> A = B )
rabeqbidv.2	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
rabeqbidv	|- ( ph -> { x e. A | ps } = { x e. B | ch } )

Distinct variable groups:   x, A   x, B   ph, x

Allowed substitution hints:   ps( x)   ch( x)

Proof of Theorem rabeqbidv

Step	Hyp	Ref	Expression
1		rabeqbidv.1	. . 3 |- ( ph -> A = B )
2		rabeq 2727	. . 3 |- ( A = B -> { x e. A | ps } = { x e. B | ps } )
3	1, 2	syl 14	. 2 |- ( ph -> { x e. A | ps } = { x e. B | ps } )
4		rabeqbidv.2	. . 3 |- ( ph -> ( ps <-> ch ) )
5	4	rabbidv 2724	. 2 |- ( ph -> { x e. B | ps } = { x e. B | ch } )
6	3, 5	eqtrd 2208	1 |- ( ph -> { x e. A | ps } = { x e. B | ch } )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353   {crab 2457

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-rab 2462

This theorem is referenced by:  elfvmptrab1  5602  mpoxopoveq  6231  supeq123d  6980  phival  12180  dfphi2  12187  ismhm  12725  issubm  12735  cldval  13179  neifval  13220  cnfval  13274  cnpfval  13275  cnprcl2k  13286  hmeofvalg  13383  ispsmet  13403  ismet  13424  isxmet  13425  blfvalps  13465  cncfval  13639