Theorem rabeqbidv 3413

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  {crab 3395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396

This theorem is referenced by:  elfvmptrab1w  6956  elfvmptrab1  6957  fvmptrabfv  6961  elovmporab1w  7593  elovmporab1  7594  ovmpt3rab1  7604  suppval  8092  mpoxopoveq  8149  supeq123d  9334  phival  16678  dfphi2  16685  hashbcval  16914  imasval  17415  ismre  17492  mrisval  17536  isacs  17557  monfval  17639  ismon  17640  monpropd  17644  natfval  17856  isnat  17857  initoval  17900  termoval  17901  gsumvalx  18584  gsumpropd  18586  gsumress  18590  ismgmhm  18604  issubmgm  18610  ismhm  18693  issubm  18711  issubg  19039  isnsg  19067  isgim  19174  isga  19203  cntzfval  19232  isslw  19520  isirred  20337  rnghmval  20358  isrngim  20363  dfrhm2  20392  isrim0  20400  issubrng  20462  issubrg  20486  rrgval  20612  issdrg  20703  abvfval  20725  lssset  20866  islmhm  20961  islmim  20996  islbs  21010  ocvfval  21603  isobs  21657  dsmmval  21671  islinds  21746  mplval  21926  mhpfval  22053  mplbaspropd  22149  dmatval  22407  scmatval  22419  cpmat  22624  cldval  22938  mretopd  23007  neifval  23014  ordtval  23104  ordtbas2  23106  ordtcnv  23116  ordtrest2  23119  cnfval  23148  cnpfval  23149  kgenval  23450  xkoval  23502  dfac14  23533  qtopval  23610  qtopval2  23611  hmeofval  23673  elmptrab  23742  fgval  23785  flimval  23878  utopval  24147  ucnval  24191  iscfilu  24202  ispsmet  24219  ismet  24238  isxmet  24239  blfvalps  24298  cncfval  24808  ishtpy  24898  isphtpy  24907  om1val  24957  cfilfval  25191  caufval  25202  cpnfval  25861  uc1pval  26072  mon1pval  26074  dchrval  27172  leftval  27804  rightval  27805  istrkgl  28436  israg  28675  iseqlg  28845  ttgval  28853  nbgrval  29314  vtxdgfval  29446  vtxdeqd  29456  1egrvtxdg1  29488  umgr2v2evd2  29506  wwlks  29813  wwlksn  29815  wspthsn  29826  wwlksnon  29829  wspthsnon  29830  iswspthsnon  29834  rusgrnumwwlklem  29951  clwwlk  29963  clwwlkn  30006  2clwwlk  30327  numclwlk1lem2  30350  numclwwlkovh0  30352  numclwwlkovq  30354  lnoval  30732  bloval  30761  hmoval  30790  mntoval  32963  tocycval  33077  fxpval  33134  fldgenval  33278  prmidlval  33402  mxidlval  33426  rprmval  33481  minplyval  33718  ordtprsuni  33932  sigagenval  34153  faeval  34259  ismbfm  34264  carsgval  34316  sitgval  34345  reprval  34623  erdszelem3  35237  erdsze  35246  kur14  35260  iscvm  35303  satf  35397  wlimeq12  35861  fwddifval  36206  poimirlem28  37687  istotbnd  37808  isbnd  37819  rngohomval  38003  rngoisoval  38016  idlval  38052  pridlval  38072  maxidlval  38078  igenval  38100  lshpset  39076  lflset  39157  pats  39383  llnset  39603  lplnset  39627  lvolset  39670  lineset  39836  pmapfval  39854  paddfval  39895  lhpset  40093  ldilfset  40206  ltrnfset  40215  ltrnset  40216  dilfsetN  40250  trnfsetN  40253  trnsetN  40254  diaffval  41128  diafval  41129  dicffval  41272  dochffval  41447  lpolsetN  41580  lcdfval  41686  lcdval  41687  mapdffval  41724  mapdfval  41725  prjcrvfval  42723  isnacs  42796  mzpclval  42817  k0004val  44242  dvnprodlem1  46043  fourierdlem2  46206  fourierdlem3  46207  etransclem12  46343  etransclem33  46364  caragenval  46590  smflimlem3  46870  fvmptrab  47391  iccpval  47514  clnbgrval  47921  isisubgr  47961  grtri  48039  stgrfv  48052  gpgov  48141  assintopval  48304  dmatALTval  48500  lcoop  48511  lines  48831  rrxlines  48833  spheres  48846