Theorem rabeqbidv 3455

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437

This theorem is referenced by:  elfvmptrab1w  7043  elfvmptrab1  7044  fvmptrabfv  7048  elovmporab1w  7680  elovmporab1  7681  ovmpt3rab1  7691  suppval  8187  mpoxopoveq  8244  supeq123d  9490  phival  16804  dfphi2  16811  hashbcval  17040  imasval  17556  ismre  17633  mrisval  17673  isacs  17694  monfval  17776  ismon  17777  monpropd  17781  natfval  17994  isnat  17995  initoval  18038  termoval  18039  gsumvalx  18689  gsumpropd  18691  gsumress  18695  ismgmhm  18709  issubmgm  18715  ismhm  18798  issubm  18816  issubg  19144  isnsg  19173  isgim  19280  isga  19309  cntzfval  19338  isslw  19626  isirred  20419  rnghmval  20440  isrngim  20445  dfrhm2  20474  isrim0OLD  20481  isrim0  20483  issubrng  20547  issubrg  20571  rrgval  20697  issdrg  20789  abvfval  20811  lssset  20931  islmhm  21026  islmim  21061  islbs  21075  ocvfval  21684  isobs  21740  dsmmval  21754  islinds  21829  mplval  22009  mhpfval  22142  mplbaspropd  22238  dmatval  22498  scmatval  22510  cpmat  22715  cldval  23031  mretopd  23100  neifval  23107  ordtval  23197  ordtbas2  23199  ordtcnv  23209  ordtrest2  23212  cnfval  23241  cnpfval  23242  kgenval  23543  xkoval  23595  dfac14  23626  qtopval  23703  qtopval2  23704  hmeofval  23766  elmptrab  23835  fgval  23878  flimval  23971  utopval  24241  ucnval  24286  iscfilu  24297  ispsmet  24314  ismet  24333  isxmet  24334  blfvalps  24393  cncfval  24914  ishtpy  25004  isphtpy  25013  om1val  25063  cfilfval  25298  caufval  25309  cpnfval  25968  uc1pval  26179  mon1pval  26181  dchrval  27278  leftval  27902  rightval  27903  istrkgl  28466  israg  28705  iseqlg  28875  ttgval  28883  ttgvalOLD  28884  nbgrval  29353  vtxdgfval  29485  vtxdeqd  29495  1egrvtxdg1  29527  umgr2v2evd2  29545  wwlks  29855  wwlksn  29857  wspthsn  29868  wwlksnon  29871  wspthsnon  29872  iswspthsnon  29876  rusgrnumwwlklem  29990  clwwlk  30002  clwwlkn  30045  2clwwlk  30366  numclwlk1lem2  30389  numclwwlkovh0  30391  numclwwlkovq  30393  lnoval  30771  bloval  30800  hmoval  30829  mntoval  32972  tocycval  33128  fldgenval  33314  prmidlval  33465  mxidlval  33489  rprmval  33544  minplyval  33748  ordtprsuni  33918  sigagenval  34141  faeval  34247  ismbfm  34252  carsgval  34305  sitgval  34334  reprval  34625  erdszelem3  35198  erdsze  35207  kur14  35221  iscvm  35264  satf  35358  wlimeq12  35820  fwddifval  36163  poimirlem28  37655  istotbnd  37776  isbnd  37787  rngohomval  37971  rngoisoval  37984  idlval  38020  pridlval  38040  maxidlval  38046  igenval  38068  lshpset  38979  lflset  39060  pats  39286  llnset  39507  lplnset  39531  lvolset  39574  lineset  39740  pmapfval  39758  paddfval  39799  lhpset  39997  ldilfset  40110  ltrnfset  40119  ltrnset  40120  dilfsetN  40154  trnfsetN  40157  trnsetN  40158  diaffval  41032  diafval  41033  dicffval  41176  dochffval  41351  lpolsetN  41484  lcdfval  41590  lcdval  41591  mapdffval  41628  mapdfval  41629  prjcrvfval  42641  isnacs  42715  mzpclval  42736  k0004val  44163  dvnprodlem1  45961  fourierdlem2  46124  fourierdlem3  46125  etransclem12  46261  etransclem33  46282  caragenval  46508  smflimlem3  46788  fvmptrab  47304  iccpval  47402  clnbgrval  47809  isisubgr  47848  grtri  47907  stgrfv  47920  gpgov  48001  assintopval  48121  dmatALTval  48317  lcoop  48328  lines  48652  rrxlines  48654  spheres  48667