MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  inteq Structured version   Visualization version   GIF version

Theorem inteq 4683
Description: Equality law for intersection. (Contributed by NM, 13-Sep-1999.)
Assertion
Ref Expression
inteq (𝐴 = 𝐵 𝐴 = 𝐵)

Proof of Theorem inteq
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 raleq 3338 . . 3 (𝐴 = 𝐵 → (∀𝑦𝐴 𝑥𝑦 ↔ ∀𝑦𝐵 𝑥𝑦))
21abbidv 2936 . 2 (𝐴 = 𝐵 → {𝑥 ∣ ∀𝑦𝐴 𝑥𝑦} = {𝑥 ∣ ∀𝑦𝐵 𝑥𝑦})
3 dfint2 4682 . 2 𝐴 = {𝑥 ∣ ∀𝑦𝐴 𝑥𝑦}
4 dfint2 4682 . 2 𝐵 = {𝑥 ∣ ∀𝑦𝐵 𝑥𝑦}
52, 3, 43eqtr4g 2876 1 (𝐴 = 𝐵 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  {cab 2803  wral 3107   cint 4680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-int 4681
This theorem is referenced by:  inteqi  4684  inteqd  4685  unissint  4704  uniintsn  4717  rint0  4720  intex  5025  intnex  5026  elreldm  5565  elxp5  7351  1stval2  7425  oev2  7850  fundmen  8276  xpsnen  8293  fiint  8486  elfir  8570  inelfi  8573  fiin  8577  cardmin2  9117  isfin2-2  9436  incexclem  14810  mreintcl  16480  ismred2  16488  fiinopn  20940  cmpfii  21447  ptbasfi  21619  fbssint  21876  shintcl  28540  chintcl  28542  inelpisys  30565  rankeq1o  32621  bj-0int  33385  bj-ismoored  33392  bj-snmoore  33398  neificl  33879  heibor1lem  33938  elrfi  37777  elrfirn  37778
  Copyright terms: Public domain W3C validator