Theorem rabeqbidv 3448

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	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		rabeqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
4	1, 3	rabeqbidva 3447	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   ∈ wcel 2105  {crab 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432

This theorem is referenced by:  elfvmptrab1w  7024  elfvmptrab1  7025  fvmptrabfv  7029  elovmporab1w  7657  elovmporab1  7658  ovmpt3rab1  7668  suppval  8152  mpoxopoveq  8208  supeq123d  9449  phival  16705  dfphi2  16712  hashbcval  16940  imasval  17462  ismre  17539  mrisval  17579  isacs  17600  monfval  17684  ismon  17685  monpropd  17689  natfval  17902  isnat  17903  initoval  17948  termoval  17949  gsumvalx  18602  gsumpropd  18604  gsumress  18608  ismgmhm  18622  issubmgm  18628  ismhm  18708  issubm  18721  issubg  19043  isnsg  19072  isgim  19177  isga  19197  cntzfval  19226  isslw  19518  isirred  20311  rnghmval  20332  isrngim  20337  dfrhm2  20366  isrim0OLD  20373  isrim0  20375  issubrng  20436  issubrg  20462  issdrg  20548  abvfval  20570  lssset  20689  islmhm  20783  islmim  20818  islbs  20832  rrgval  21104  ocvfval  21439  isobs  21495  dsmmval  21509  islinds  21584  mplval  21768  mhpfval  21902  mplbaspropd  21980  dmatval  22215  scmatval  22227  cpmat  22432  cldval  22748  mretopd  22817  neifval  22824  ordtval  22914  ordtbas2  22916  ordtcnv  22926  ordtrest2  22929  cnfval  22958  cnpfval  22959  kgenval  23260  xkoval  23312  dfac14  23343  qtopval  23420  qtopval2  23421  hmeofval  23483  elmptrab  23552  fgval  23595  flimval  23688  utopval  23958  ucnval  24003  iscfilu  24014  ispsmet  24031  ismet  24050  isxmet  24051  blfvalps  24110  cncfval  24629  ishtpy  24719  isphtpy  24728  om1val  24778  cfilfval  25013  caufval  25024  cpnfval  25683  uc1pval  25893  mon1pval  25895  dchrval  26974  leftval  27596  rightval  27597  istrkgl  27977  israg  28216  iseqlg  28386  ttgval  28394  ttgvalOLD  28395  nbgrval  28861  vtxdgfval  28992  vtxdeqd  29002  1egrvtxdg1  29034  umgr2v2evd2  29052  wwlks  29357  wwlksn  29359  wspthsn  29370  wwlksnon  29373  wspthsnon  29374  iswspthsnon  29378  rusgrnumwwlklem  29492  clwwlk  29504  clwwlkn  29547  2clwwlk  29868  numclwlk1lem2  29891  numclwwlkovh0  29893  numclwwlkovq  29895  lnoval  30273  bloval  30302  hmoval  30331  mntoval  32420  tocycval  32538  fldgenval  32673  prmidlval  32830  mxidlval  32852  rprmval  32908  minplyval  33056  ordtprsuni  33198  sigagenval  33437  faeval  33543  ismbfm  33548  carsgval  33601  sitgval  33630  reprval  33921  erdszelem3  34483  erdsze  34492  kur14  34506  iscvm  34549  satf  34643  wlimeq12  35096  fwddifval  35439  poimirlem28  36820  istotbnd  36941  isbnd  36952  rngohomval  37136  rngoisoval  37149  idlval  37185  pridlval  37205  maxidlval  37211  igenval  37233  lshpset  38152  lflset  38233  pats  38459  llnset  38680  lplnset  38704  lvolset  38747  lineset  38913  pmapfval  38931  paddfval  38972  lhpset  39170  ldilfset  39283  ltrnfset  39292  ltrnset  39293  dilfsetN  39327  trnfsetN  39330  trnsetN  39331  diaffval  40205  diafval  40206  dicffval  40349  dochffval  40524  lpolsetN  40657  lcdfval  40763  lcdval  40764  mapdffval  40801  mapdfval  40802  prjcrvfval  41676  isnacs  41745  mzpclval  41766  k0004val  43204  fourierdlem2  45124  fourierdlem3  45125  etransclem12  45261  etransclem33  45282  caragenval  45508  smflimlem3  45788  fvmptrab  46299  iccpval  46382  assintopval  46882  dmatALTval  47169  lcoop  47180  lines  47505  rrxlines  47507  spheres  47520