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

Theorem inteq 4909
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 3308 . . 3 (𝐴 = 𝐵 → (∀𝑦𝐴 𝑥𝑦 ↔ ∀𝑦𝐵 𝑥𝑦))
21abbidv 2807 . 2 (𝐴 = 𝐵 → {𝑥 ∣ ∀𝑦𝐴 𝑥𝑦} = {𝑥 ∣ ∀𝑦𝐵 𝑥𝑦})
3 dfint2 4908 . 2 𝐴 = {𝑥 ∣ ∀𝑦𝐴 𝑥𝑦}
4 dfint2 4908 . 2 𝐵 = {𝑥 ∣ ∀𝑦𝐵 𝑥𝑦}
52, 3, 43eqtr4g 2803 1 (𝐴 = 𝐵 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  {cab 2715  wral 3063   cint 4906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-ral 3064  df-int 4907
This theorem is referenced by:  inteqi  4910  inteqd  4911  unissint  4932  uniintsn  4947  rint0  4950  intex  5293  intnex  5294  elreldm  5887  elxp5  7851  1stval2  7929  oev2  8437  fundmen  8909  xpsnen  8933  fiint  9202  elfir  9285  inelfi  9288  fiin  9292  cardmin2  9869  isfin2-2  10189  incexclem  15657  mreintcl  17411  ismred2  17419  fiinopn  22178  cmpfii  22688  ptbasfi  22860  fbssint  23117  shintcl  30077  chintcl  30079  zarcmplem  32242  inelpisys  32533  rankeq1o  34687  bj-0int  35503  bj-ismoored  35509  bj-snmoore  35515  bj-prmoore  35517  neificl  36143  heibor1lem  36199  elrfi  40919  elrfirn  40920
  Copyright terms: Public domain W3C validator