Theorem rabeqbidv 3462

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 group:   𝜑,𝑥

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 3460	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108  {crab 3443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444

This theorem is referenced by:  elfvmptrab1w  7056  elfvmptrab1  7057  fvmptrabfv  7061  elovmporab1w  7697  elovmporab1  7698  ovmpt3rab1  7708  suppval  8203  mpoxopoveq  8260  supeq123d  9519  phival  16814  dfphi2  16821  hashbcval  17049  imasval  17571  ismre  17648  mrisval  17688  isacs  17709  monfval  17793  ismon  17794  monpropd  17798  natfval  18014  isnat  18015  initoval  18060  termoval  18061  gsumvalx  18714  gsumpropd  18716  gsumress  18720  ismgmhm  18734  issubmgm  18740  ismhm  18820  issubm  18838  issubg  19166  isnsg  19195  isgim  19302  isga  19331  cntzfval  19360  isslw  19650  isirred  20445  rnghmval  20466  isrngim  20471  dfrhm2  20500  isrim0OLD  20507  isrim0  20509  issubrng  20573  issubrg  20599  rrgval  20719  issdrg  20811  abvfval  20833  lssset  20954  islmhm  21049  islmim  21084  islbs  21098  ocvfval  21707  isobs  21763  dsmmval  21777  islinds  21852  mplval  22032  mhpfval  22165  mplbaspropd  22259  dmatval  22519  scmatval  22531  cpmat  22736  cldval  23052  mretopd  23121  neifval  23128  ordtval  23218  ordtbas2  23220  ordtcnv  23230  ordtrest2  23233  cnfval  23262  cnpfval  23263  kgenval  23564  xkoval  23616  dfac14  23647  qtopval  23724  qtopval2  23725  hmeofval  23787  elmptrab  23856  fgval  23899  flimval  23992  utopval  24262  ucnval  24307  iscfilu  24318  ispsmet  24335  ismet  24354  isxmet  24355  blfvalps  24414  cncfval  24933  ishtpy  25023  isphtpy  25032  om1val  25082  cfilfval  25317  caufval  25328  cpnfval  25988  uc1pval  26199  mon1pval  26201  dchrval  27296  leftval  27920  rightval  27921  istrkgl  28484  israg  28723  iseqlg  28893  ttgval  28901  ttgvalOLD  28902  nbgrval  29371  vtxdgfval  29503  vtxdeqd  29513  1egrvtxdg1  29545  umgr2v2evd2  29563  wwlks  29868  wwlksn  29870  wspthsn  29881  wwlksnon  29884  wspthsnon  29885  iswspthsnon  29889  rusgrnumwwlklem  30003  clwwlk  30015  clwwlkn  30058  2clwwlk  30379  numclwlk1lem2  30402  numclwwlkovh0  30404  numclwwlkovq  30406  lnoval  30784  bloval  30813  hmoval  30842  mntoval  32955  tocycval  33101  fldgenval  33279  prmidlval  33430  mxidlval  33454  rprmval  33509  minplyval  33698  ordtprsuni  33865  sigagenval  34104  faeval  34210  ismbfm  34215  carsgval  34268  sitgval  34297  reprval  34587  erdszelem3  35161  erdsze  35170  kur14  35184  iscvm  35227  satf  35321  wlimeq12  35783  fwddifval  36126  poimirlem28  37608  istotbnd  37729  isbnd  37740  rngohomval  37924  rngoisoval  37937  idlval  37973  pridlval  37993  maxidlval  37999  igenval  38021  lshpset  38934  lflset  39015  pats  39241  llnset  39462  lplnset  39486  lvolset  39529  lineset  39695  pmapfval  39713  paddfval  39754  lhpset  39952  ldilfset  40065  ltrnfset  40074  ltrnset  40075  dilfsetN  40109  trnfsetN  40112  trnsetN  40113  diaffval  40987  diafval  40988  dicffval  41131  dochffval  41306  lpolsetN  41439  lcdfval  41545  lcdval  41546  mapdffval  41583  mapdfval  41584  prjcrvfval  42586  isnacs  42660  mzpclval  42681  k0004val  44112  fourierdlem2  46030  fourierdlem3  46031  etransclem12  46167  etransclem33  46188  caragenval  46414  smflimlem3  46694  fvmptrab  47207  iccpval  47289  clnbgrval  47696  isisubgr  47734  grtri  47791  assintopval  47928  dmatALTval  48129  lcoop  48140  lines  48465  rrxlines  48467  spheres  48480