Theorem rabeqbidv 3411

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548   ∈ wcel 2121  {crab 3393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394

This theorem is referenced by:  elfvmptrab1w  6967  elfvmptrab1  6968  fvmptrabfv  6972  elovmporab1w  7607  elovmporab1  7608  ovmpt3rab1  7618  suppval  8106  mpoxopoveq  8163  supeq123d  9357  phival  16732  dfphi2  16739  hashbcval  16968  imasval  17470  ismre  17547  mrisval  17591  isacs  17612  monfval  17694  ismon  17695  monpropd  17699  natfval  17911  isnat  17912  initoval  17955  termoval  17956  gsumvalx  18639  gsumpropd  18641  gsumress  18645  ismgmhm  18659  issubmgm  18665  ismhm  18748  issubm  18766  issubg  19097  isnsg  19125  isgim  19232  isga  19261  cntzfval  19290  isslw  19578  isirred  20394  rnghmval  20415  isrngim  20420  dfrhm2  20449  isrim0  20457  issubrng  20523  issubrg  20547  rrgval  20673  issdrg  20764  abvfval  20786  lssset  20927  islmhm  21021  islmim  21056  islbs  21070  ocvfval  21645  isobs  21699  dsmmval  21713  islinds  21788  mplval  21967  mhpfval  22130  mplbaspropd  22225  dmatval  22479  scmatval  22491  cpmat  22696  cldval  23010  mretopd  23079  neifval  23086  ordtval  23176  ordtbas2  23178  ordtcnv  23188  ordtrest2  23191  cnfval  23220  cnpfval  23221  kgenval  23522  xkoval  23574  dfac14  23605  qtopval  23682  qtopval2  23683  hmeofval  23745  elmptrab  23814  fgval  23857  flimval  23950  utopval  24219  ucnval  24263  iscfilu  24274  ispsmet  24291  ismet  24310  isxmet  24311  blfvalps  24370  cncfval  24877  ishtpy  24961  isphtpy  24970  om1val  25019  cfilfval  25253  caufval  25264  cpnfval  25921  uc1pval  26127  mon1pval  26129  dchrval  27219  leftval  27863  rightval  27864  istrkgl  28548  israg  28787  iseqlg  28957  ttgval  28965  nbgrval  29427  vtxdgfval  29558  vtxdeqd  29568  1egrvtxdg1  29600  umgr2v2evd2  29618  wwlks  29925  wwlksn  29927  wspthsn  29938  wwlksnon  29941  wspthsnon  29942  iswspthsnon  29946  rusgrnumwwlklem  30063  clwwlk  30075  clwwlkn  30118  2clwwlk  30439  numclwlk1lem2  30462  numclwwlkovh0  30464  numclwwlkovq  30466  lnoval  30845  bloval  30874  hmoval  30903  mntoval  33065  tocycval  33193  fxpval  33250  fldgenval  33400  prmidlval  33524  mxidlval  33548  rprmval  33611  minplyval  33901  ordtprsuni  34115  sigagenval  34336  faeval  34442  ismbfm  34447  carsgval  34499  sitgval  34528  reprval  34806  erdszelem3  35436  erdsze  35445  kur14  35459  iscvm  35502  satf  35596  wlimeq12  36060  fwddifval  36405  poimirlem28  38030  istotbnd  38151  isbnd  38162  rngohomval  38346  rngoisoval  38359  idlval  38395  pridlval  38415  maxidlval  38421  igenval  38443  lshpset  39485  lflset  39566  pats  39792  llnset  40012  lplnset  40036  lvolset  40079  lineset  40245  pmapfval  40263  paddfval  40304  lhpset  40502  ldilfset  40615  ltrnfset  40624  ltrnset  40625  dilfsetN  40659  trnfsetN  40662  trnsetN  40663  diaffval  41537  diafval  41538  dicffval  41681  dochffval  41856  lpolsetN  41989  lcdfval  42095  lcdval  42096  mapdffval  42133  mapdfval  42134  prjcrvfval  43096  isnacs  43168  mzpclval  43189  k0004val  44609  dvnprodlem1  46403  fourierdlem2  46566  fourierdlem3  46567  etransclem12  46703  etransclem33  46724  caragenval  46950  smflimlem3  47230  fvmptrab  47769  iccpval  47904  clnbgrval  48327  isisubgr  48367  grtri  48445  stgrfv  48458  gpgov  48547  assintopval  48710  dmatALTval  48905  lcoop  48916  lines  49236  rrxlines  49238  spheres  49251