Theorem rabeqbidv 3413

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395

This theorem is referenced by:  elfvmptrab1w  6957  elfvmptrab1  6958  fvmptrabfv  6962  elovmporab1w  7596  elovmporab1  7597  ovmpt3rab1  7607  suppval  8095  mpoxopoveq  8152  supeq123d  9340  phival  16678  dfphi2  16685  hashbcval  16914  imasval  17415  ismre  17492  mrisval  17536  isacs  17557  monfval  17639  ismon  17640  monpropd  17644  natfval  17856  isnat  17857  initoval  17900  termoval  17901  gsumvalx  18550  gsumpropd  18552  gsumress  18556  ismgmhm  18570  issubmgm  18576  ismhm  18659  issubm  18677  issubg  19005  isnsg  19034  isgim  19141  isga  19170  cntzfval  19199  isslw  19487  isirred  20304  rnghmval  20325  isrngim  20330  dfrhm2  20359  isrim0OLD  20366  isrim0  20368  issubrng  20432  issubrg  20456  rrgval  20582  issdrg  20673  abvfval  20695  lssset  20836  islmhm  20931  islmim  20966  islbs  20980  ocvfval  21573  isobs  21627  dsmmval  21641  islinds  21716  mplval  21896  mhpfval  22023  mplbaspropd  22119  dmatval  22377  scmatval  22389  cpmat  22594  cldval  22908  mretopd  22977  neifval  22984  ordtval  23074  ordtbas2  23076  ordtcnv  23086  ordtrest2  23089  cnfval  23118  cnpfval  23119  kgenval  23420  xkoval  23472  dfac14  23503  qtopval  23580  qtopval2  23581  hmeofval  23643  elmptrab  23712  fgval  23755  flimval  23848  utopval  24118  ucnval  24162  iscfilu  24173  ispsmet  24190  ismet  24209  isxmet  24210  blfvalps  24269  cncfval  24779  ishtpy  24869  isphtpy  24878  om1val  24928  cfilfval  25162  caufval  25173  cpnfval  25832  uc1pval  26043  mon1pval  26045  dchrval  27143  leftval  27775  rightval  27776  istrkgl  28407  israg  28646  iseqlg  28816  ttgval  28824  nbgrval  29285  vtxdgfval  29417  vtxdeqd  29427  1egrvtxdg1  29459  umgr2v2evd2  29477  wwlks  29784  wwlksn  29786  wspthsn  29797  wwlksnon  29800  wspthsnon  29801  iswspthsnon  29805  rusgrnumwwlklem  29919  clwwlk  29931  clwwlkn  29974  2clwwlk  30295  numclwlk1lem2  30318  numclwwlkovh0  30320  numclwwlkovq  30322  lnoval  30700  bloval  30729  hmoval  30758  mntoval  32933  tocycval  33059  fxpval  33116  fldgenval  33260  prmidlval  33383  mxidlval  33407  rprmval  33462  minplyval  33688  ordtprsuni  33902  sigagenval  34123  faeval  34229  ismbfm  34234  carsgval  34287  sitgval  34316  reprval  34594  erdszelem3  35186  erdsze  35195  kur14  35209  iscvm  35252  satf  35346  wlimeq12  35813  fwddifval  36156  poimirlem28  37648  istotbnd  37769  isbnd  37780  rngohomval  37964  rngoisoval  37977  idlval  38013  pridlval  38033  maxidlval  38039  igenval  38061  lshpset  38977  lflset  39058  pats  39284  llnset  39504  lplnset  39528  lvolset  39571  lineset  39737  pmapfval  39755  paddfval  39796  lhpset  39994  ldilfset  40107  ltrnfset  40116  ltrnset  40117  dilfsetN  40151  trnfsetN  40154  trnsetN  40155  diaffval  41029  diafval  41030  dicffval  41173  dochffval  41348  lpolsetN  41481  lcdfval  41587  lcdval  41588  mapdffval  41625  mapdfval  41626  prjcrvfval  42624  isnacs  42697  mzpclval  42718  k0004val  44143  dvnprodlem1  45947  fourierdlem2  46110  fourierdlem3  46111  etransclem12  46247  etransclem33  46268  caragenval  46494  smflimlem3  46774  fvmptrab  47296  iccpval  47419  clnbgrval  47826  isisubgr  47866  grtri  47944  stgrfv  47957  gpgov  48046  assintopval  48209  dmatALTval  48405  lcoop  48416  lines  48736  rrxlines  48738  spheres  48751