Theorem rabeqbidv 3433

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

Hypotheses

Ref	Expression
rabeqbidv.1	⊢ (𝜑 → 𝐴 = 𝐵)
rabeqbidv.2	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rabeqbidv	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem rabeqbidv

Step	Hyp	Ref	Expression
1		rabeqbidv.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	rabeqdv 3432	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
3		rabeqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	3	rabbidv 3427	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
5	2, 4	eqtrd 2833	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  {crab 3110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115

This theorem is referenced by:  elfvmptrab1w  6771  elfvmptrab1  6772  fvmptrabfv  6776  elovmporab1w  7372  elovmporab1  7373  ovmpt3rab1  7383  suppval  7815  mpoxopoveq  7868  supeq123d  8898  phival  16094  dfphi2  16101  hashbcval  16328  imasval  16776  ismre  16853  mrisval  16893  isacs  16914  monfval  16994  ismon  16995  monpropd  16999  natfval  17208  isnat  17209  initoval  17249  termoval  17250  gsumvalx  17878  gsumpropd  17880  gsumress  17884  ismhm  17950  issubm  17960  issubg  18271  isnsg  18299  isgim  18394  isga  18413  cntzfval  18442  isslw  18725  isirred  19445  dfrhm2  19465  isrim0  19471  issubrg  19528  issdrg  19567  abvfval  19582  lssset  19698  islmhm  19792  islmim  19827  islbs  19841  rrgval  20053  ocvfval  20355  isobs  20409  dsmmval  20423  islinds  20498  mplval  20666  mhpfval  20791  mplbaspropd  20866  dmatval  21097  scmatval  21109  cpmat  21314  cldval  21628  mretopd  21697  neifval  21704  ordtval  21794  ordtbas2  21796  ordtcnv  21806  ordtrest2  21809  cnfval  21838  cnpfval  21839  kgenval  22140  xkoval  22192  dfac14  22223  qtopval  22300  qtopval2  22301  hmeofval  22363  elmptrab  22432  fgval  22475  flimval  22568  utopval  22838  ucnval  22883  iscfilu  22894  ispsmet  22911  ismet  22930  isxmet  22931  blfvalps  22990  cncfval  23493  ishtpy  23577  isphtpy  23586  om1val  23635  cfilfval  23868  caufval  23879  cpnfval  24535  uc1pval  24740  mon1pval  24742  dchrval  25818  istrkgl  26252  israg  26491  iseqlg  26661  ttgval  26669  nbgrval  27126  vtxdgfval  27257  vtxdeqd  27267  1egrvtxdg1  27299  umgr2v2evd2  27317  wwlks  27621  wwlksn  27623  wspthsn  27634  wwlksnon  27637  wspthsnon  27638  iswspthsnon  27642  rusgrnumwwlklem  27756  clwwlk  27768  clwwlkn  27811  2clwwlk  28132  numclwlk1lem2  28155  numclwwlkovh0  28157  numclwwlkovq  28159  lnoval  28535  bloval  28564  hmoval  28593  mntoval  30690  tocycval  30800  prmidlval  31020  mxidlval  31041  rprmval  31072  ordtprsuni  31272  sigagenval  31509  faeval  31615  ismbfm  31620  carsgval  31671  sitgval  31700  reprval  31991  erdszelem3  32553  erdsze  32562  kur14  32576  iscvm  32619  satf  32713  wlimeq12  33219  fwddifval  33736  poimirlem28  35085  istotbnd  35207  isbnd  35218  rngohomval  35402  rngoisoval  35415  idlval  35451  pridlval  35471  maxidlval  35477  igenval  35499  lshpset  36274  lflset  36355  pats  36581  llnset  36801  lplnset  36825  lvolset  36868  lineset  37034  pmapfval  37052  paddfval  37093  lhpset  37291  ldilfset  37404  ltrnfset  37413  ltrnset  37414  dilfsetN  37448  trnfsetN  37451  trnsetN  37452  diaffval  38326  diafval  38327  dicffval  38470  dochffval  38645  lpolsetN  38778  lcdfval  38884  lcdval  38885  mapdffval  38922  mapdfval  38923  isnacs  39645  mzpclval  39666  k0004val  40853  fourierdlem2  42751  fourierdlem3  42752  etransclem12  42888  etransclem33  42909  caragenval  43132  smflimlem3  43406  fvmptrab  43848  iccpval  43932  ismgmhm  44403  issubmgm  44409  assintopval  44465  rnghmval  44515  isrngisom  44520  dmatALTval  44809  lcoop  44820  lines  45145  rrxlines  45147  spheres  45160