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

Theorem inteq 4844
 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 3361 . . 3 (𝐴 = 𝐵 → (∀𝑦𝐴 𝑥𝑦 ↔ ∀𝑦𝐵 𝑥𝑦))
21abbidv 2865 . 2 (𝐴 = 𝐵 → {𝑥 ∣ ∀𝑦𝐴 𝑥𝑦} = {𝑥 ∣ ∀𝑦𝐵 𝑥𝑦})
3 dfint2 4843 . 2 𝐴 = {𝑥 ∣ ∀𝑦𝐴 𝑥𝑦}
4 dfint2 4843 . 2 𝐵 = {𝑥 ∣ ∀𝑦𝐵 𝑥𝑦}
52, 3, 43eqtr4g 2861 1 (𝐴 = 𝐵 𝐴 = 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538  {cab 2779  ∀wral 3109  ∩ cint 4841 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ral 3114  df-int 4842 This theorem is referenced by:  inteqi  4845  inteqd  4846  unissint  4865  uniintsn  4878  rint0  4881  intex  5207  intnex  5208  elreldm  5773  elxp5  7614  1stval2  7692  oev2  8135  fundmen  8570  xpsnen  8588  fiint  8783  elfir  8867  inelfi  8870  fiin  8874  cardmin2  9416  isfin2-2  9734  incexclem  15186  mreintcl  16861  ismred2  16869  fiinopn  21509  cmpfii  22017  ptbasfi  22189  fbssint  22446  shintcl  29116  chintcl  29118  zarcmplem  31234  inelpisys  31521  rankeq1o  33740  bj-0int  34511  bj-ismoored  34517  bj-snmoore  34523  bj-prmoore  34525  neificl  35184  heibor1lem  35240  elrfi  39622  elrfirn  39623
 Copyright terms: Public domain W3C validator