Theorem rabeqbidv 3416

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399

This theorem is referenced by:  elfvmptrab1w  6968  elfvmptrab1  6969  fvmptrabfv  6973  elovmporab1w  7605  elovmporab1  7606  ovmpt3rab1  7616  suppval  8104  mpoxopoveq  8161  supeq123d  9355  phival  16696  dfphi2  16703  hashbcval  16932  imasval  17434  ismre  17511  mrisval  17555  isacs  17576  monfval  17658  ismon  17659  monpropd  17663  natfval  17875  isnat  17876  initoval  17919  termoval  17920  gsumvalx  18603  gsumpropd  18605  gsumress  18609  ismgmhm  18623  issubmgm  18629  ismhm  18712  issubm  18730  issubg  19058  isnsg  19086  isgim  19193  isga  19222  cntzfval  19251  isslw  19539  isirred  20357  rnghmval  20378  isrngim  20383  dfrhm2  20412  isrim0  20420  issubrng  20482  issubrg  20506  rrgval  20632  issdrg  20723  abvfval  20745  lssset  20886  islmhm  20981  islmim  21016  islbs  21030  ocvfval  21623  isobs  21677  dsmmval  21691  islinds  21766  mplval  21946  mhpfval  22083  mplbaspropd  22179  dmatval  22438  scmatval  22450  cpmat  22655  cldval  22969  mretopd  23038  neifval  23045  ordtval  23135  ordtbas2  23137  ordtcnv  23147  ordtrest2  23150  cnfval  23179  cnpfval  23180  kgenval  23481  xkoval  23533  dfac14  23564  qtopval  23641  qtopval2  23642  hmeofval  23704  elmptrab  23773  fgval  23816  flimval  23909  utopval  24178  ucnval  24222  iscfilu  24233  ispsmet  24250  ismet  24269  isxmet  24270  blfvalps  24329  cncfval  24839  ishtpy  24929  isphtpy  24938  om1val  24988  cfilfval  25222  caufval  25233  cpnfval  25892  uc1pval  26103  mon1pval  26105  dchrval  27203  leftval  27839  rightval  27840  istrkgl  28511  israg  28750  iseqlg  28920  ttgval  28928  nbgrval  29390  vtxdgfval  29522  vtxdeqd  29532  1egrvtxdg1  29564  umgr2v2evd2  29582  wwlks  29889  wwlksn  29891  wspthsn  29902  wwlksnon  29905  wspthsnon  29906  iswspthsnon  29910  rusgrnumwwlklem  30027  clwwlk  30039  clwwlkn  30082  2clwwlk  30403  numclwlk1lem2  30426  numclwwlkovh0  30428  numclwwlkovq  30430  lnoval  30808  bloval  30837  hmoval  30866  mntoval  33043  tocycval  33169  fxpval  33226  fldgenval  33373  prmidlval  33497  mxidlval  33521  rprmval  33576  minplyval  33841  ordtprsuni  34055  sigagenval  34276  faeval  34382  ismbfm  34387  carsgval  34439  sitgval  34468  reprval  34746  erdszelem3  35366  erdsze  35375  kur14  35389  iscvm  35432  satf  35526  wlimeq12  35990  fwddifval  36335  poimirlem28  37818  istotbnd  37939  isbnd  37950  rngohomval  38134  rngoisoval  38147  idlval  38183  pridlval  38203  maxidlval  38209  igenval  38231  lshpset  39273  lflset  39354  pats  39580  llnset  39800  lplnset  39824  lvolset  39867  lineset  40033  pmapfval  40051  paddfval  40092  lhpset  40290  ldilfset  40403  ltrnfset  40412  ltrnset  40413  dilfsetN  40447  trnfsetN  40450  trnsetN  40451  diaffval  41325  diafval  41326  dicffval  41469  dochffval  41644  lpolsetN  41777  lcdfval  41883  lcdval  41884  mapdffval  41921  mapdfval  41922  prjcrvfval  42911  isnacs  42983  mzpclval  43004  k0004val  44428  dvnprodlem1  46227  fourierdlem2  46390  fourierdlem3  46391  etransclem12  46527  etransclem33  46548  caragenval  46774  smflimlem3  47054  fvmptrab  47575  iccpval  47698  clnbgrval  48105  isisubgr  48145  grtri  48223  stgrfv  48236  gpgov  48325  assintopval  48488  dmatALTval  48683  lcoop  48694  lines  49014  rrxlines  49016  spheres  49029