Theorem rabeqbidv 3408

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {crab 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391

This theorem is referenced by:  elfvmptrab1w  6971  elfvmptrab1  6972  fvmptrabfv  6976  elovmporab1w  7609  elovmporab1  7610  ovmpt3rab1  7620  suppval  8107  mpoxopoveq  8164  supeq123d  9358  phival  16732  dfphi2  16739  hashbcval  16968  imasval  17470  ismre  17547  mrisval  17591  isacs  17612  monfval  17694  ismon  17695  monpropd  17699  natfval  17911  isnat  17912  initoval  17955  termoval  17956  gsumvalx  18639  gsumpropd  18641  gsumress  18645  ismgmhm  18659  issubmgm  18665  ismhm  18748  issubm  18766  issubg  19097  isnsg  19125  isgim  19232  isga  19261  cntzfval  19290  isslw  19578  isirred  20394  rnghmval  20415  isrngim  20420  dfrhm2  20449  isrim0  20457  issubrng  20519  issubrg  20543  rrgval  20669  issdrg  20760  abvfval  20782  lssset  20923  islmhm  21018  islmim  21053  islbs  21067  ocvfval  21660  isobs  21714  dsmmval  21728  islinds  21803  mplval  21981  mhpfval  22118  mplbaspropd  22214  dmatval  22471  scmatval  22483  cpmat  22688  cldval  23002  mretopd  23071  neifval  23078  ordtval  23168  ordtbas2  23170  ordtcnv  23180  ordtrest2  23183  cnfval  23212  cnpfval  23213  kgenval  23514  xkoval  23566  dfac14  23597  qtopval  23674  qtopval2  23675  hmeofval  23737  elmptrab  23806  fgval  23849  flimval  23942  utopval  24211  ucnval  24255  iscfilu  24266  ispsmet  24283  ismet  24302  isxmet  24303  blfvalps  24362  cncfval  24869  ishtpy  24953  isphtpy  24962  om1val  25011  cfilfval  25245  caufval  25256  cpnfval  25913  uc1pval  26119  mon1pval  26121  dchrval  27215  leftval  27859  rightval  27860  istrkgl  28544  israg  28783  iseqlg  28953  ttgval  28961  nbgrval  29423  vtxdgfval  29555  vtxdeqd  29565  1egrvtxdg1  29597  umgr2v2evd2  29615  wwlks  29922  wwlksn  29924  wspthsn  29935  wwlksnon  29938  wspthsnon  29939  iswspthsnon  29943  rusgrnumwwlklem  30060  clwwlk  30072  clwwlkn  30115  2clwwlk  30436  numclwlk1lem2  30459  numclwwlkovh0  30461  numclwwlkovq  30463  lnoval  30842  bloval  30871  hmoval  30900  mntoval  33061  tocycval  33188  fxpval  33245  fldgenval  33392  prmidlval  33516  mxidlval  33540  rprmval  33595  minplyval  33869  ordtprsuni  34083  sigagenval  34304  faeval  34410  ismbfm  34415  carsgval  34467  sitgval  34496  reprval  34774  erdszelem3  35395  erdsze  35404  kur14  35418  iscvm  35461  satf  35555  wlimeq12  36019  fwddifval  36364  poimirlem28  37989  istotbnd  38110  isbnd  38121  rngohomval  38305  rngoisoval  38318  idlval  38354  pridlval  38374  maxidlval  38380  igenval  38402  lshpset  39444  lflset  39525  pats  39751  llnset  39971  lplnset  39995  lvolset  40038  lineset  40204  pmapfval  40222  paddfval  40263  lhpset  40461  ldilfset  40574  ltrnfset  40583  ltrnset  40584  dilfsetN  40618  trnfsetN  40621  trnsetN  40622  diaffval  41496  diafval  41497  dicffval  41640  dochffval  41815  lpolsetN  41948  lcdfval  42054  lcdval  42055  mapdffval  42092  mapdfval  42093  prjcrvfval  43084  isnacs  43156  mzpclval  43177  k0004val  44601  dvnprodlem1  46398  fourierdlem2  46561  fourierdlem3  46562  etransclem12  46698  etransclem33  46719  caragenval  46945  smflimlem3  47225  fvmptrab  47758  iccpval  47893  clnbgrval  48316  isisubgr  48356  grtri  48434  stgrfv  48447  gpgov  48536  assintopval  48699  dmatALTval  48894  lcoop  48905  lines  49225  rrxlines  49227  spheres  49240