Theorem rabeqbidv 3433

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2142  {crab 3415

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416

This theorem is used by:  elfvmptrab1w  7017  elfvmptrab1  7018  fvmptrabfv  7022  elovmporab1w  7659  elovmporab1  7660  ovmpt3rab1  7670  suppval  8156  mpoxopoveq  8213  supeq123d  9408  phival  16832  dfphi2  16839  hashbcval  17068  imasval  17571  ismre  17648  mrisval  17692  isacs  17713  monfval  17795  ismon  17796  monpropd  17800  natfval  18012  isnat  18013  initoval  18056  termoval  18057  gsumvalx  18740  gsumpropd  18742  gsumress  18746  ismgmhm  18760  issubmgm  18766  ismhm  18849  issubm  18867  issubg  19198  isnsg  19227  isgim  19338  isga  19367  cntzfval  19396  isslw  19684  isirred  20508  rnghmval  20529  isrngim  20534  dfrhm2  20563  rhmval0  20564  isrim0  20572  issubrng  20657  issubrg  20681  rrgval  20807  issdrg  20902  abvfval  20924  lssset  21065  islmhm  21159  islmim  21194  islbs  21208  prmidlval  21473  ocvfval  21827  isobs  21881  dsmmval  21895  islinds  21970  mplval  22149  mhpfval  22312  mplbaspropd  22407  dmatval  22660  scmatval  22672  cpmat  22877  cldval  23191  mretopd  23260  neifval  23267  ordtval  23357  ordtbas2  23359  ordtcnv  23369  ordtrest2  23372  cnfval  23401  cnpfval  23402  kgenval  23703  xkoval  23755  dfac14  23786  qtopval  23863  qtopval2  23864  hmeofval  23926  elmptrab  23995  fgval  24038  flimval  24131  utopval  24400  ucnval  24444  iscfilu  24455  ispsmet  24472  ismet  24491  isxmet  24492  blfvalps  24551  cncfval  25058  ishtpy  25142  isphtpy  25151  om1val  25200  cfilfval  25434  caufval  25445  cpnfval  26102  uc1pval  26308  mon1pval  26310  dchrval  27409  leftval  28053  rightval  28054  istrkgl  28738  israg  28988  tgplnfn  29068  plngval  29070  isplng  29071  iseqlg  29195  ttgval  29235  nbgrval  29697  vtxdgfval  29828  vtxdeqd  29838  1egrvtxdg1  29870  umgr2v2evd2  29888  wwlks  30195  wwlksn  30197  wspthsn  30208  wwlksnon  30211  wspthsnon  30212  iswspthsnon  30216  rusgrnumwwlklem  30333  clwwlk  30345  clwwlkn  30388  2clwwlk  30709  numclwlk1lem2  30732  numclwwlkovh0  30734  numclwwlkovq  30736  lnoval  31115  bloval  31144  hmoval  31173  mntoval  33311  tocycval  33437  fxpval  33494  fldgenval  33642  mxidlval  33753  rprmval  33815  minplyval  34104  ordtprsuni  34318  sigagenval  34539  faeval  34645  ismbfm  34650  carsgval  34702  sitgval  34731  reprval  35006  erdszelem3  35693  erdsze  35702  kur14  35716  iscvm  35759  satf  35853  wlimeq12  36317  fwddifval  36662  poimirlem28  38327  istotbnd  38448  isbnd  38459  rngohomval  38643  rngoisoval  38656  idlval  38692  pridlval  38712  maxidlval  38718  igenval  38740  lshpset  39780  lflset  39861  pats  40087  llnset  40307  lplnset  40331  lvolset  40374  lineset  40540  pmapfval  40558  paddfval  40599  lhpset  40797  ldilfset  40910  ltrnfset  40919  ltrnset  40920  dilfsetN  40954  trnfsetN  40957  trnsetN  40958  diaffval  41832  diafval  41833  dicffval  41976  dochffval  42151  lpolsetN  42284  lcdfval  42390  lcdval  42391  mapdffval  42428  mapdfval  42429  prjcrvfval  43391  isnacs  43463  mzpclval  43484  k0004val  44904  dvnprodlem1  46688  fourierdlem2  46851  fourierdlem3  46852  etransclem12  46988  etransclem33  47009  caragenval  47235  smflimlem3  47515  fvmptrab  48057  iccpval  48192  clnbgrval  48615  isisubgr  48655  grtri  48733  stgrfv  48746  gpgov  48835  assintopval  48998  dmatALTval  49208  lcoop  49219  lines  49539  rrxlines  49541  spheres  49554