Theorem rabeqbidv 3421

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403

This theorem is referenced by:  elfvmptrab1w  6977  elfvmptrab1  6978  fvmptrabfv  6982  elovmporab1w  7616  elovmporab1  7617  ovmpt3rab1  7627  suppval  8118  mpoxopoveq  8175  supeq123d  9377  phival  16713  dfphi2  16720  hashbcval  16949  imasval  17450  ismre  17527  mrisval  17571  isacs  17592  monfval  17674  ismon  17675  monpropd  17679  natfval  17891  isnat  17892  initoval  17935  termoval  17936  gsumvalx  18585  gsumpropd  18587  gsumress  18591  ismgmhm  18605  issubmgm  18611  ismhm  18694  issubm  18712  issubg  19040  isnsg  19069  isgim  19176  isga  19205  cntzfval  19234  isslw  19522  isirred  20339  rnghmval  20360  isrngim  20365  dfrhm2  20394  isrim0OLD  20401  isrim0  20403  issubrng  20467  issubrg  20491  rrgval  20617  issdrg  20708  abvfval  20730  lssset  20871  islmhm  20966  islmim  21001  islbs  21015  ocvfval  21608  isobs  21662  dsmmval  21676  islinds  21751  mplval  21931  mhpfval  22058  mplbaspropd  22154  dmatval  22412  scmatval  22424  cpmat  22629  cldval  22943  mretopd  23012  neifval  23019  ordtval  23109  ordtbas2  23111  ordtcnv  23121  ordtrest2  23124  cnfval  23153  cnpfval  23154  kgenval  23455  xkoval  23507  dfac14  23538  qtopval  23615  qtopval2  23616  hmeofval  23678  elmptrab  23747  fgval  23790  flimval  23883  utopval  24153  ucnval  24197  iscfilu  24208  ispsmet  24225  ismet  24244  isxmet  24245  blfvalps  24304  cncfval  24814  ishtpy  24904  isphtpy  24913  om1val  24963  cfilfval  25197  caufval  25208  cpnfval  25867  uc1pval  26078  mon1pval  26080  dchrval  27178  leftval  27808  rightval  27809  istrkgl  28438  israg  28677  iseqlg  28847  ttgval  28855  nbgrval  29316  vtxdgfval  29448  vtxdeqd  29458  1egrvtxdg1  29490  umgr2v2evd2  29508  wwlks  29815  wwlksn  29817  wspthsn  29828  wwlksnon  29831  wspthsnon  29832  iswspthsnon  29836  rusgrnumwwlklem  29950  clwwlk  29962  clwwlkn  30005  2clwwlk  30326  numclwlk1lem2  30349  numclwwlkovh0  30351  numclwwlkovq  30353  lnoval  30731  bloval  30760  hmoval  30789  mntoval  32954  tocycval  33080  fxpval  33137  fldgenval  33278  prmidlval  33401  mxidlval  33425  rprmval  33480  minplyval  33688  ordtprsuni  33902  sigagenval  34123  faeval  34229  ismbfm  34234  carsgval  34287  sitgval  34316  reprval  34594  erdszelem3  35173  erdsze  35182  kur14  35196  iscvm  35239  satf  35333  wlimeq12  35800  fwddifval  36143  poimirlem28  37635  istotbnd  37756  isbnd  37767  rngohomval  37951  rngoisoval  37964  idlval  38000  pridlval  38020  maxidlval  38026  igenval  38048  lshpset  38964  lflset  39045  pats  39271  llnset  39492  lplnset  39516  lvolset  39559  lineset  39725  pmapfval  39743  paddfval  39784  lhpset  39982  ldilfset  40095  ltrnfset  40104  ltrnset  40105  dilfsetN  40139  trnfsetN  40142  trnsetN  40143  diaffval  41017  diafval  41018  dicffval  41161  dochffval  41336  lpolsetN  41469  lcdfval  41575  lcdval  41576  mapdffval  41613  mapdfval  41614  prjcrvfval  42612  isnacs  42685  mzpclval  42706  k0004val  44132  dvnprodlem1  45937  fourierdlem2  46100  fourierdlem3  46101  etransclem12  46237  etransclem33  46258  caragenval  46484  smflimlem3  46764  fvmptrab  47286  iccpval  47409  clnbgrval  47816  isisubgr  47855  grtri  47932  stgrfv  47945  gpgov  48026  assintopval  48186  dmatALTval  48382  lcoop  48393  lines  48713  rrxlines  48715  spheres  48728