Theorem rabeqbidv 3427

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409

This theorem is referenced by:  elfvmptrab1w  6998  elfvmptrab1  6999  fvmptrabfv  7003  elovmporab1w  7639  elovmporab1  7640  ovmpt3rab1  7650  suppval  8144  mpoxopoveq  8201  supeq123d  9408  phival  16744  dfphi2  16751  hashbcval  16980  imasval  17481  ismre  17558  mrisval  17598  isacs  17619  monfval  17701  ismon  17702  monpropd  17706  natfval  17918  isnat  17919  initoval  17962  termoval  17963  gsumvalx  18610  gsumpropd  18612  gsumress  18616  ismgmhm  18630  issubmgm  18636  ismhm  18719  issubm  18737  issubg  19065  isnsg  19094  isgim  19201  isga  19230  cntzfval  19259  isslw  19545  isirred  20335  rnghmval  20356  isrngim  20361  dfrhm2  20390  isrim0OLD  20397  isrim0  20399  issubrng  20463  issubrg  20487  rrgval  20613  issdrg  20704  abvfval  20726  lssset  20846  islmhm  20941  islmim  20976  islbs  20990  ocvfval  21582  isobs  21636  dsmmval  21650  islinds  21725  mplval  21905  mhpfval  22032  mplbaspropd  22128  dmatval  22386  scmatval  22398  cpmat  22603  cldval  22917  mretopd  22986  neifval  22993  ordtval  23083  ordtbas2  23085  ordtcnv  23095  ordtrest2  23098  cnfval  23127  cnpfval  23128  kgenval  23429  xkoval  23481  dfac14  23512  qtopval  23589  qtopval2  23590  hmeofval  23652  elmptrab  23721  fgval  23764  flimval  23857  utopval  24127  ucnval  24171  iscfilu  24182  ispsmet  24199  ismet  24218  isxmet  24219  blfvalps  24278  cncfval  24788  ishtpy  24878  isphtpy  24887  om1val  24937  cfilfval  25171  caufval  25182  cpnfval  25841  uc1pval  26052  mon1pval  26054  dchrval  27152  leftval  27778  rightval  27779  istrkgl  28392  israg  28631  iseqlg  28801  ttgval  28809  nbgrval  29270  vtxdgfval  29402  vtxdeqd  29412  1egrvtxdg1  29444  umgr2v2evd2  29462  wwlks  29772  wwlksn  29774  wspthsn  29785  wwlksnon  29788  wspthsnon  29789  iswspthsnon  29793  rusgrnumwwlklem  29907  clwwlk  29919  clwwlkn  29962  2clwwlk  30283  numclwlk1lem2  30306  numclwwlkovh0  30308  numclwwlkovq  30310  lnoval  30688  bloval  30717  hmoval  30746  mntoval  32915  tocycval  33072  fxpval  33129  fldgenval  33269  prmidlval  33415  mxidlval  33439  rprmval  33494  minplyval  33702  ordtprsuni  33916  sigagenval  34137  faeval  34243  ismbfm  34248  carsgval  34301  sitgval  34330  reprval  34608  erdszelem3  35187  erdsze  35196  kur14  35210  iscvm  35253  satf  35347  wlimeq12  35814  fwddifval  36157  poimirlem28  37649  istotbnd  37770  isbnd  37781  rngohomval  37965  rngoisoval  37978  idlval  38014  pridlval  38034  maxidlval  38040  igenval  38062  lshpset  38978  lflset  39059  pats  39285  llnset  39506  lplnset  39530  lvolset  39573  lineset  39739  pmapfval  39757  paddfval  39798  lhpset  39996  ldilfset  40109  ltrnfset  40118  ltrnset  40119  dilfsetN  40153  trnfsetN  40156  trnsetN  40157  diaffval  41031  diafval  41032  dicffval  41175  dochffval  41350  lpolsetN  41483  lcdfval  41589  lcdval  41590  mapdffval  41627  mapdfval  41628  prjcrvfval  42626  isnacs  42699  mzpclval  42720  k0004val  44146  dvnprodlem1  45951  fourierdlem2  46114  fourierdlem3  46115  etransclem12  46251  etransclem33  46272  caragenval  46498  smflimlem3  46778  fvmptrab  47297  iccpval  47420  clnbgrval  47827  isisubgr  47866  grtri  47943  stgrfv  47956  gpgov  48037  assintopval  48197  dmatALTval  48393  lcoop  48404  lines  48724  rrxlines  48726  spheres  48739