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

Theorem inteq 4870
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 3403 . . 3 (𝐴 = 𝐵 → (∀𝑦𝐴 𝑥𝑦 ↔ ∀𝑦𝐵 𝑥𝑦))
21abbidv 2882 . 2 (𝐴 = 𝐵 → {𝑥 ∣ ∀𝑦𝐴 𝑥𝑦} = {𝑥 ∣ ∀𝑦𝐵 𝑥𝑦})
3 dfint2 4869 . 2 𝐴 = {𝑥 ∣ ∀𝑦𝐴 𝑥𝑦}
4 dfint2 4869 . 2 𝐵 = {𝑥 ∣ ∀𝑦𝐵 𝑥𝑦}
52, 3, 43eqtr4g 2878 1 (𝐴 = 𝐵 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  {cab 2796  wral 3135   cint 4867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-ral 3140  df-int 4868
This theorem is referenced by:  inteqi  4871  inteqd  4872  unissint  4891  uniintsn  4904  rint0  4907  intex  5231  intnex  5232  elreldm  5798  elxp5  7617  1stval2  7695  oev2  8137  fundmen  8571  xpsnen  8589  fiint  8783  elfir  8867  inelfi  8870  fiin  8874  cardmin2  9415  isfin2-2  9729  incexclem  15179  mreintcl  16854  ismred2  16862  fiinopn  21437  cmpfii  21945  ptbasfi  22117  fbssint  22374  shintcl  29034  chintcl  29036  inelpisys  31312  rankeq1o  33529  bj-0int  34287  bj-ismoored  34293  bj-snmoore  34299  neificl  34909  heibor1lem  34968  elrfi  39169  elrfirn  39170
  Copyright terms: Public domain W3C validator