Theorem rabeqbidv 3434

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1562   ∈ wcel 2144  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417

This theorem is referenced by:  elfvmptrab1w  7005  elfvmptrab1  7006  fvmptrabfv  7010  elovmporab1w  7645  elovmporab1  7646  ovmpt3rab1  7656  suppval  8144  mpoxopoveq  8201  supeq123d  9398  phival  16804  dfphi2  16811  hashbcval  17040  imasval  17543  ismre  17620  mrisval  17664  isacs  17685  monfval  17767  ismon  17768  monpropd  17772  natfval  17984  isnat  17985  initoval  18028  termoval  18029  gsumvalx  18712  gsumpropd  18714  gsumress  18718  ismgmhm  18732  issubmgm  18738  ismhm  18821  issubm  18839  issubg  19170  isnsg  19198  isgim  19304  isga  19333  cntzfval  19362  isslw  19650  isirred  20470  rnghmval  20491  isrngim  20496  dfrhm2  20525  isrim0  20533  issubrng  20599  issubrg  20623  rrgval  20749  issdrg  20839  abvfval  20861  lssset  21002  islmhm  21096  islmim  21131  islbs  21145  ocvfval  21720  isobs  21774  dsmmval  21788  islinds  21863  mplval  22042  mhpfval  22205  mplbaspropd  22300  dmatval  22554  scmatval  22566  cpmat  22771  cldval  23085  mretopd  23154  neifval  23161  ordtval  23251  ordtbas2  23253  ordtcnv  23263  ordtrest2  23266  cnfval  23295  cnpfval  23296  kgenval  23597  xkoval  23649  dfac14  23680  qtopval  23757  qtopval2  23758  hmeofval  23820  elmptrab  23889  fgval  23932  flimval  24025  utopval  24294  ucnval  24338  iscfilu  24349  ispsmet  24366  ismet  24385  isxmet  24386  blfvalps  24445  cncfval  24952  ishtpy  25036  isphtpy  25045  om1val  25094  cfilfval  25328  caufval  25339  cpnfval  25996  uc1pval  26202  mon1pval  26204  dchrval  27300  leftval  27944  rightval  27945  istrkgl  28629  israg  28872  tgplnfn  28984  plngval  28986  isplng  28987  iseqlg  29063  ttgval  29077  nbgrval  29539  vtxdgfval  29670  vtxdeqd  29680  1egrvtxdg1  29712  umgr2v2evd2  29730  wwlks  30037  wwlksn  30039  wspthsn  30050  wwlksnon  30053  wspthsnon  30054  iswspthsnon  30058  rusgrnumwwlklem  30175  clwwlk  30187  clwwlkn  30230  2clwwlk  30551  numclwlk1lem2  30574  numclwwlkovh0  30576  numclwwlkovq  30578  lnoval  30957  bloval  30986  hmoval  31015  mntoval  33162  tocycval  33290  fxpval  33347  fldgenval  33501  prmidlval  33625  mxidlval  33651  rprmval  33714  minplyval  34004  ordtprsuni  34218  sigagenval  34439  faeval  34545  ismbfm  34550  carsgval  34602  sitgval  34631  reprval  34906  erdszelem3  35548  erdsze  35557  kur14  35571  iscvm  35614  satf  35708  wlimeq12  36172  fwddifval  36517  poimirlem28  38152  istotbnd  38273  isbnd  38284  rngohomval  38468  rngoisoval  38481  idlval  38517  pridlval  38537  maxidlval  38543  igenval  38565  lshpset  39607  lflset  39688  pats  39914  llnset  40134  lplnset  40158  lvolset  40201  lineset  40367  pmapfval  40385  paddfval  40426  lhpset  40624  ldilfset  40737  ltrnfset  40746  ltrnset  40747  dilfsetN  40781  trnfsetN  40784  trnsetN  40785  diaffval  41659  diafval  41660  dicffval  41803  dochffval  41978  lpolsetN  42111  lcdfval  42217  lcdval  42218  mapdffval  42255  mapdfval  42256  prjcrvfval  43218  isnacs  43290  mzpclval  43311  k0004val  44731  dvnprodlem1  46525  fourierdlem2  46688  fourierdlem3  46689  etransclem12  46825  etransclem33  46846  caragenval  47072  smflimlem3  47352  fvmptrab  47891  iccpval  48026  clnbgrval  48449  isisubgr  48489  grtri  48567  stgrfv  48580  gpgov  48669  assintopval  48832  dmatALTval  49027  lcoop  49038  lines  49358  rrxlines  49360  spheres  49373