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

Theorem inteq 4948
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 3322 . . 3 (𝐴 = 𝐵 → (∀𝑦𝐴 𝑥𝑦 ↔ ∀𝑦𝐵 𝑥𝑦))
21abbidv 2807 . 2 (𝐴 = 𝐵 → {𝑥 ∣ ∀𝑦𝐴 𝑥𝑦} = {𝑥 ∣ ∀𝑦𝐵 𝑥𝑦})
3 dfint2 4947 . 2 𝐴 = {𝑥 ∣ ∀𝑦𝐴 𝑥𝑦}
4 dfint2 4947 . 2 𝐵 = {𝑥 ∣ ∀𝑦𝐵 𝑥𝑦}
52, 3, 43eqtr4g 2801 1 (𝐴 = 𝐵 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  {cab 2713  wral 3060   cint 4945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-ral 3061  df-rex 3070  df-int 4946
This theorem is referenced by:  inteqi  4949  inteqd  4950  unissint  4971  uniintsn  4984  rint0  4987  intex  5343  intnex  5344  elreldm  5945  elxp5  7946  1stval2  8032  oev2  8562  fundmen  9072  xpsnen  9096  fiint  9367  fiintOLD  9368  elfir  9456  inelfi  9459  fiin  9463  cardmin2  10040  isfin2-2  10360  incexclem  15873  mreintcl  17639  ismred2  17647  fiinopn  22908  cmpfii  23418  ptbasfi  23590  fbssint  23847  shintcl  31350  chintcl  31352  zarcmplem  33881  inelpisys  34156  rankeq1o  36173  bj-0int  37103  bj-ismoored  37109  bj-snmoore  37115  bj-prmoore  37117  neificl  37761  heibor1lem  37817  elrfi  42710  elrfirn  42711
  Copyright terms: Public domain W3C validator