Theorem rabeqbidv 3407

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390

This theorem is referenced by:  elfvmptrab1w  6975  elfvmptrab1  6976  fvmptrabfv  6980  elovmporab1w  7614  elovmporab1  7615  ovmpt3rab1  7625  suppval  8112  mpoxopoveq  8169  supeq123d  9363  phival  16737  dfphi2  16744  hashbcval  16973  imasval  17475  ismre  17552  mrisval  17596  isacs  17617  monfval  17699  ismon  17700  monpropd  17704  natfval  17916  isnat  17917  initoval  17960  termoval  17961  gsumvalx  18644  gsumpropd  18646  gsumress  18650  ismgmhm  18664  issubmgm  18670  ismhm  18753  issubm  18771  issubg  19102  isnsg  19130  isgim  19237  isga  19266  cntzfval  19295  isslw  19583  isirred  20399  rnghmval  20420  isrngim  20425  dfrhm2  20454  isrim0  20462  issubrng  20524  issubrg  20548  rrgval  20674  issdrg  20765  abvfval  20787  lssset  20928  islmhm  21022  islmim  21057  islbs  21071  ocvfval  21646  isobs  21700  dsmmval  21714  islinds  21789  mplval  21967  mhpfval  22104  mplbaspropd  22200  dmatval  22457  scmatval  22469  cpmat  22674  cldval  22988  mretopd  23057  neifval  23064  ordtval  23154  ordtbas2  23156  ordtcnv  23166  ordtrest2  23169  cnfval  23198  cnpfval  23199  kgenval  23500  xkoval  23552  dfac14  23583  qtopval  23660  qtopval2  23661  hmeofval  23723  elmptrab  23792  fgval  23835  flimval  23928  utopval  24197  ucnval  24241  iscfilu  24252  ispsmet  24269  ismet  24288  isxmet  24289  blfvalps  24348  cncfval  24855  ishtpy  24939  isphtpy  24948  om1val  24997  cfilfval  25231  caufval  25242  cpnfval  25899  uc1pval  26105  mon1pval  26107  dchrval  27197  leftval  27841  rightval  27842  istrkgl  28526  israg  28765  iseqlg  28935  ttgval  28943  nbgrval  29405  vtxdgfval  29536  vtxdeqd  29546  1egrvtxdg1  29578  umgr2v2evd2  29596  wwlks  29903  wwlksn  29905  wspthsn  29916  wwlksnon  29919  wspthsnon  29920  iswspthsnon  29924  rusgrnumwwlklem  30041  clwwlk  30053  clwwlkn  30096  2clwwlk  30417  numclwlk1lem2  30440  numclwwlkovh0  30442  numclwwlkovq  30444  lnoval  30823  bloval  30852  hmoval  30881  mntoval  33042  tocycval  33169  fxpval  33226  fldgenval  33373  prmidlval  33497  mxidlval  33521  rprmval  33576  minplyval  33849  ordtprsuni  34063  sigagenval  34284  faeval  34390  ismbfm  34395  carsgval  34447  sitgval  34476  reprval  34754  erdszelem3  35375  erdsze  35384  kur14  35398  iscvm  35441  satf  35535  wlimeq12  35999  fwddifval  36344  poimirlem28  37969  istotbnd  38090  isbnd  38101  rngohomval  38285  rngoisoval  38298  idlval  38334  pridlval  38354  maxidlval  38360  igenval  38382  lshpset  39424  lflset  39505  pats  39731  llnset  39951  lplnset  39975  lvolset  40018  lineset  40184  pmapfval  40202  paddfval  40243  lhpset  40441  ldilfset  40554  ltrnfset  40563  ltrnset  40564  dilfsetN  40598  trnfsetN  40601  trnsetN  40602  diaffval  41476  diafval  41477  dicffval  41620  dochffval  41795  lpolsetN  41928  lcdfval  42034  lcdval  42035  mapdffval  42072  mapdfval  42073  prjcrvfval  43064  isnacs  43136  mzpclval  43157  k0004val  44577  dvnprodlem1  46374  fourierdlem2  46537  fourierdlem3  46538  etransclem12  46674  etransclem33  46695  caragenval  46921  smflimlem3  47201  fvmptrab  47740  iccpval  47875  clnbgrval  48298  isisubgr  48338  grtri  48416  stgrfv  48429  gpgov  48518  assintopval  48681  dmatALTval  48876  lcoop  48887  lines  49207  rrxlines  49209  spheres  49222