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

Theorem inteq 4612
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 3286 . . 3 (𝐴 = 𝐵 → (∀𝑦𝐴 𝑥𝑦 ↔ ∀𝑦𝐵 𝑥𝑦))
21abbidv 2889 . 2 (𝐴 = 𝐵 → {𝑥 ∣ ∀𝑦𝐴 𝑥𝑦} = {𝑥 ∣ ∀𝑦𝐵 𝑥𝑦})
3 dfint2 4611 . 2 𝐴 = {𝑥 ∣ ∀𝑦𝐴 𝑥𝑦}
4 dfint2 4611 . 2 𝐵 = {𝑥 ∣ ∀𝑦𝐵 𝑥𝑦}
52, 3, 43eqtr4g 2829 1 (𝐴 = 𝐵 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1630  {cab 2756  wral 3060   cint 4609
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-int 4610
This theorem is referenced by:  inteqi  4613  inteqd  4614  unissint  4633  uniintsn  4646  rint0  4649  intex  4948  intnex  4949  elreldm  5488  elxp5  7257  1stval2  7331  oev2  7756  fundmen  8182  xpsnen  8199  fiint  8392  elfir  8476  inelfi  8479  fiin  8483  cardmin2  9023  isfin2-2  9342  incexclem  14774  mreintcl  16462  ismred2  16470  fiinopn  20925  cmpfii  21432  ptbasfi  21604  fbssint  21861  shintcl  28523  chintcl  28525  inelpisys  30551  rankeq1o  32609  bj-0int  33380  bj-ismoored  33387  bj-snmoore  33393  neificl  33874  heibor1lem  33933  elrfi  37776  elrfirn  37777
  Copyright terms: Public domain W3C validator