Theorem rabeqbidv 3432

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {crab 3414

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415

This theorem is used by:  elfvmptrab1w  7018  elfvmptrab1  7019  fvmptrabfv  7023  elovmporab1w  7664  elovmporab1  7665  ovmpt3rab1  7675  suppval  8163  mpoxopoveq  8220  supeq123d  9423  phival  16862  dfphi2  16869  hashbcval  17098  imasval  17601  ismre  17678  mrisval  17722  isacs  17743  monfval  17825  ismon  17826  monpropd  17830  natfval  18042  isnat  18043  initoval  18086  termoval  18087  gsumvalx  18780  gsumpropd  18782  gsumress  18786  ismgmhm  18800  issubmgm  18806  ismhm  18894  issubm  18912  issubg  19250  isnsg  19279  isgim  19390  isga  19419  cntzfval  19448  isslw  19736  isirred  20561  rnghmval  20582  isrngim  20587  dfrhm2  20616  rhmval0  20617  isrim0  20625  issubrng  20710  issubrg  20734  rrgval  20860  issdrg  20955  abvfval  20977  lssset  21118  islmhm  21212  islmim  21247  islbs  21261  prmidlval  21526  ocvfval  21880  isobs  21934  dsmmval  21948  islinds  22023  mplval  22204  mhpfval  22367  mplbaspropd  22462  dmatval  22715  scmatval  22727  cpmat  22935  cldval  23249  mretopd  23318  neifval  23325  ordtval  23415  ordtbas2  23417  ordtcnv  23427  ordtrest2  23430  cnfval  23459  cnpfval  23460  kgenval  23762  xkoval  23814  dfac14  23845  qtopval  23922  qtopval2  23923  hmeofval  23985  elmptrab  24054  fgval  24097  flimval  24190  utopval  24459  ucnval  24503  iscfilu  24514  ispsmet  24531  ismet  24550  isxmet  24551  blfvalps  24610  cncfval  25117  ishtpy  25201  isphtpy  25210  om1val  25259  cfilfval  25493  caufval  25504  cpnfval  26161  uc1pval  26367  mon1pval  26369  dchrval  27468  leftval  28112  rightval  28113  istrkgl  28797  israg  29049  tgplnfn  29130  plngval  29132  isplng  29133  iseqlg  29277  ttgval  29317  nbgrval  29782  vtxdgfval  29913  vtxdeqd  29923  1egrvtxdg1  29955  umgr2v2evd2  29973  wwlks  30289  wwlksn  30291  wspthsn  30302  wwlksnon  30305  wspthsnon  30306  iswspthsnon  30310  rusgrnumwwlklem  30427  clwwlk  30439  clwwlkn  30482  2clwwlk  30813  numclwlk1lem2  30836  numclwwlkovh0  30838  numclwwlkovq  30840  lnoval  31219  bloval  31248  hmoval  31277  mntoval  33409  tocycval  33535  fxpval  33592  fldgenval  33740  mxidlval  33851  rprmval  33913  minplyval  34202  ordtprsuni  34416  sigagenval  34638  faeval  34744  ismbfm  34749  carsgval  34801  sitgval  34830  reprval  35105  erdszelem3  35759  erdsze  35768  kur14  35782  iscvm  35825  satf  35919  wlimeq12  36383  fwddifval  36729  poimirlem28  38384  istotbnd  38506  isbnd  38517  rngohomval  38701  rngoisoval  38714  idlval  38750  pridlval  38770  maxidlval  38776  igenval  38798  lshpset  39838  lflset  39919  pats  40145  llnset  40365  lplnset  40389  lvolset  40432  lineset  40598  pmapfval  40616  paddfval  40657  lhpset  40855  ldilfset  40968  ltrnfset  40977  ltrnset  40978  dilfsetN  41012  trnfsetN  41015  trnsetN  41016  diaffval  41890  diafval  41891  dicffval  42034  dochffval  42209  lpolsetN  42342  lcdfval  42448  lcdval  42449  mapdffval  42486  mapdfval  42487  prjcrvfval  43464  isnacs  43536  mzpclval  43557  k0004val  44977  dvnprodlem1  46761  fourierdlem2  46924  fourierdlem3  46925  etransclem12  47061  etransclem33  47082  caragenval  47308  smflimlem3  47588  fvmptrab  48167  iccpval  48302  clnbgrval  48725  isisubgr  48765  grtri  48843  stgrfv  48856  gpgov  48945  assintopval  49107  dmatALTval  49317  lcoop  49328  lines  49648  rrxlines  49650  spheres  49663