Theorem rabeqbidv 3168

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 groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem rabeqbidv

Step	Hyp	Ref	Expression
1		rabeqbidv.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	rabeqdv 3167	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
3		rabeqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	3	rabbidv 3164	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
5	2, 4	eqtrd 2644	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  {crab 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905

This theorem is referenced by:  elfvmptrab1  6213  elovmpt2rab1  6779  ovmpt3rab1  6789  suppval  7184  mpt2xopoveq  7232  supeq123d  8239  phival  15310  dfphi2  15317  hashbcval  15544  imasval  15994  ismre  16073  mrisval  16113  isacs  16135  monfval  16215  ismon  16216  monpropd  16220  natfval  16429  isnat  16430  initoval  16470  termoval  16471  gsumvalx  17093  gsumpropd  17095  gsumress  17099  ismhm  17160  issubm  17170  issubg  17417  isnsg  17446  isgim  17527  isga  17547  cntzfval  17576  isslw  17846  isirred  18522  dfrhm2  18540  isrim0  18546  issubrg  18603  abvfval  18641  lssset  18755  islmhm  18848  islmim  18883  islbs  18897  rrgval  19108  mplval  19249  mplbaspropd  19428  ocvfval  19829  isobs  19883  dsmmval  19897  islinds  19967  dmatval  20117  scmatval  20129  cpmat  20333  cldval  20637  mretopd  20706  neifval  20713  ordtval  20803  ordtbas2  20805  ordtcnv  20815  ordtrest2  20818  cnfval  20847  cnpfval  20848  kgenval  21148  xkoval  21200  dfac14  21231  qtopval  21308  qtopval2  21309  hmeofval  21371  elmptrab  21440  fgval  21484  flimval  21577  utopval  21846  ucnval  21891  iscfilu  21902  ispsmet  21919  ismet  21938  isxmet  21939  blfvalps  21998  cncfval  22499  ishtpy  22579  isphtpy  22588  om1val  22638  cfilfval  22870  caufval  22881  cpnfval  23501  uc1pval  23703  mon1pval  23705  dchrval  24759  istrkgl  25157  israg  25392  iseqlg  25547  ttgval  25555  nbgraop  25952  isuvtx  26016  wwlk  26209  clwwlk  26294  is2wlkonot  26390  is2spthonot  26391  2wlksot  26394  2spthsot  26395  2wlkonot3v  26402  2spthonot3v  26403  vdgrfval  26422  rusgranumwlklem2  26477  numclwwlkovf  26608  numclwwlkovg  26614  numclwwlkovq  26626  numclwwlkovh  26628  numclwwlk5  26639  lnoval  26991  bloval  27020  hmoval  27049  ordtprsuni  29293  sigagenval  29530  faeval  29636  ismbfm  29641  carsgval  29692  sitgval  29721  erdszelem3  30429  erdsze  30438  kur14  30452  iscvm  30495  wlimeq12  31009  fwddifval  31439  poimirlem28  32607  istotbnd  32738  isbnd  32749  rngohomval  32933  rngoisoval  32946  idlval  32982  pridlval  33002  maxidlval  33008  igenval  33030  lshpset  33283  lflset  33364  pats  33590  llnset  33809  lplnset  33833  lvolset  33876  lineset  34042  pmapfval  34060  paddfval  34101  lhpset  34299  ldilfset  34412  ltrnfset  34421  ltrnset  34422  dilfsetN  34457  trnfsetN  34460  trnsetN  34461  diaffval  35337  diafval  35338  dicffval  35481  dochffval  35656  lpolsetN  35789  lcdfval  35895  lcdval  35896  mapdffval  35933  mapdfval  35934  isnacs  36285  mzpclval  36306  issdrg  36786  k0004val  37468  fourierdlem2  39002  fourierdlem3  39003  etransclem12  39139  etransclem33  39160  caragenval  39383  smflimlem3  39659  iccpval  39953  nbgrval  40560  uvtxaval  40613  vtxdgfval  40683  vtxdeqd  40692  1egrvtxdg1  40725  umgr2v2evd2  40743  wwlks  41038  wwlksn  41040  wspthsn  41046  wwlksnon  41049  wspthsnon  41050  iswspthsnon  41052  rusgrnumwwlklem  41173  clwwlks  41187  clwwlksn  41189  av-numclwwlkovf  41511  av-numclwwlkovg  41518  av-numclwwlkovq  41529  av-numclwwlkovh  41531  av-numclwwlk5  41542  ismgmhm  41573  issubmgm  41579  assintopval  41631  rnghmval  41681  isrngisom  41686  dmatALTval  41983  lcoop  41994