Theorem rabeqbidv 2536

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

Proof of Theorem rabeqbidv

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

Syntax hints:   -> wi 3   <-> wb 219   = wceq 1586  {crab 2358

This theorem is referenced by:  aceq8clem 6201  fodomnum 6209  supcvg 8877  ubos2 15337  mxlelt2 15345  mxlelt 15346  mnlelt2 15347  mnlmxl2 15350  rngisoval 16955  idlval 16985  pridlval 17005  maxidlval 17011  pats 17676  plusssfval 17916  ocvfval 17918  llnset 17937  lplnset 17960  lvolset 18004  lineset 18171  pmapfval 18188  paddfval 18229  lhpset 18408  ldilfset 18462  ltrnfset 18470  ltrnset 18471  dilfset 18497  trnfset 18500  trnset 18501

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-ex 1616  df-sb 1816  df-clab 2129  df-cleq 2134  df-clel 2137  df-rab 2362

Copyright terms: Public domain