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

Theorem inteq 4630
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 3277 . . 3 (𝐴 = 𝐵 → (∀𝑦𝐴 𝑥𝑦 ↔ ∀𝑦𝐵 𝑥𝑦))
21abbidv 2879 . 2 (𝐴 = 𝐵 → {𝑥 ∣ ∀𝑦𝐴 𝑥𝑦} = {𝑥 ∣ ∀𝑦𝐵 𝑥𝑦})
3 dfint2 4629 . 2 𝐴 = {𝑥 ∣ ∀𝑦𝐴 𝑥𝑦}
4 dfint2 4629 . 2 𝐵 = {𝑥 ∣ ∀𝑦𝐵 𝑥𝑦}
52, 3, 43eqtr4g 2819 1 (𝐴 = 𝐵 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  {cab 2746  wral 3050   cint 4627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-int 4628
This theorem is referenced by:  inteqi  4631  inteqd  4632  unissint  4653  uniintsn  4666  rint0  4669  intex  4969  intnex  4970  elreldm  5505  elxp5  7277  1stval2  7351  oev2  7774  fundmen  8197  xpsnen  8211  fiint  8404  elfir  8488  inelfi  8491  fiin  8495  cardmin2  9034  isfin2-2  9353  incexclem  14787  mreintcl  16477  ismred2  16485  fiinopn  20928  cmpfii  21434  ptbasfi  21606  fbssint  21863  shintcl  28519  chintcl  28521  inelpisys  30547  rankeq1o  32605  bj-0int  33379  bj-ismoored  33386  bj-snmoore  33392  neificl  33880  heibor1lem  33939  elrfi  37777  elrfirn  37778
  Copyright terms: Public domain W3C validator