Theorem rabeqbidv 3418

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

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

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 3401

This theorem is referenced by:  elfvmptrab1w  6970  elfvmptrab1  6971  fvmptrabfv  6975  elovmporab1w  7607  elovmporab1  7608  ovmpt3rab1  7618  suppval  8106  mpoxopoveq  8163  supeq123d  9357  phival  16698  dfphi2  16705  hashbcval  16934  imasval  17436  ismre  17513  mrisval  17557  isacs  17578  monfval  17660  ismon  17661  monpropd  17665  natfval  17877  isnat  17878  initoval  17921  termoval  17922  gsumvalx  18605  gsumpropd  18607  gsumress  18611  ismgmhm  18625  issubmgm  18631  ismhm  18714  issubm  18732  issubg  19060  isnsg  19088  isgim  19195  isga  19224  cntzfval  19253  isslw  19541  isirred  20359  rnghmval  20380  isrngim  20385  dfrhm2  20414  isrim0  20422  issubrng  20484  issubrg  20508  rrgval  20634  issdrg  20725  abvfval  20747  lssset  20888  islmhm  20983  islmim  21018  islbs  21032  ocvfval  21625  isobs  21679  dsmmval  21693  islinds  21768  mplval  21948  mhpfval  22085  mplbaspropd  22181  dmatval  22440  scmatval  22452  cpmat  22657  cldval  22971  mretopd  23040  neifval  23047  ordtval  23137  ordtbas2  23139  ordtcnv  23149  ordtrest2  23152  cnfval  23181  cnpfval  23182  kgenval  23483  xkoval  23535  dfac14  23566  qtopval  23643  qtopval2  23644  hmeofval  23706  elmptrab  23775  fgval  23818  flimval  23911  utopval  24180  ucnval  24224  iscfilu  24235  ispsmet  24252  ismet  24271  isxmet  24272  blfvalps  24331  cncfval  24841  ishtpy  24931  isphtpy  24940  om1val  24990  cfilfval  25224  caufval  25235  cpnfval  25894  uc1pval  26105  mon1pval  26107  dchrval  27205  leftval  27849  rightval  27850  istrkgl  28534  israg  28773  iseqlg  28943  ttgval  28951  nbgrval  29413  vtxdgfval  29545  vtxdeqd  29555  1egrvtxdg1  29587  umgr2v2evd2  29605  wwlks  29912  wwlksn  29914  wspthsn  29925  wwlksnon  29928  wspthsnon  29929  iswspthsnon  29933  rusgrnumwwlklem  30050  clwwlk  30062  clwwlkn  30105  2clwwlk  30426  numclwlk1lem2  30449  numclwwlkovh0  30451  numclwwlkovq  30453  lnoval  30831  bloval  30860  hmoval  30889  mntoval  33066  tocycval  33192  fxpval  33249  fldgenval  33396  prmidlval  33520  mxidlval  33544  rprmval  33599  minplyval  33864  ordtprsuni  34078  sigagenval  34299  faeval  34405  ismbfm  34410  carsgval  34462  sitgval  34491  reprval  34769  erdszelem3  35389  erdsze  35398  kur14  35412  iscvm  35455  satf  35549  wlimeq12  36013  fwddifval  36358  poimirlem28  37851  istotbnd  37972  isbnd  37983  rngohomval  38167  rngoisoval  38180  idlval  38216  pridlval  38236  maxidlval  38242  igenval  38264  lshpset  39306  lflset  39387  pats  39613  llnset  39833  lplnset  39857  lvolset  39900  lineset  40066  pmapfval  40084  paddfval  40125  lhpset  40323  ldilfset  40436  ltrnfset  40445  ltrnset  40446  dilfsetN  40480  trnfsetN  40483  trnsetN  40484  diaffval  41358  diafval  41359  dicffval  41502  dochffval  41677  lpolsetN  41810  lcdfval  41916  lcdval  41917  mapdffval  41954  mapdfval  41955  prjcrvfval  42941  isnacs  43013  mzpclval  43034  k0004val  44458  dvnprodlem1  46257  fourierdlem2  46420  fourierdlem3  46421  etransclem12  46557  etransclem33  46578  caragenval  46804  smflimlem3  47084  fvmptrab  47605  iccpval  47728  clnbgrval  48135  isisubgr  48175  grtri  48253  stgrfv  48266  gpgov  48355  assintopval  48518  dmatALTval  48713  lcoop  48724  lines  49044  rrxlines  49046  spheres  49059