Theorem inteq 4892

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.

Step	Hyp	Ref	Expression
1		raleq 3292	. . 3 ⊢ (𝐴 = 𝐵 → (∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦))
2	1	abbidv 2802	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} = {𝑥 ∣ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦})
3		dfint2 4891	. 2 ⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦}
4		dfint2 4891	. 2 ⊢ ∩ 𝐵 = {𝑥 ∣ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦}
5	2, 3, 4	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)

Syntax hints:   → wi 4   = wceq 1542  {cab 2714  ∀wral 3051  ∩ cint 4889

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-ral 3052  df-rex 3062  df-int 4890

This theorem is referenced by:  inteqi  4893  inteqd  4894  unissint  4914  uniintsn  4927  rint0  4930  intex  5285  intnex  5286  elreldm  5890  elxp5  7874  1stval2  7959  oev2  8458  fundmen  8978  xpsnen  8999  fiint  9237  elfir  9328  inelfi  9331  fiin  9335  cardmin2  9923  isfin2-2  10241  incexclem  15801  mreintcl  17557  ismred2  17565  fiinopn  22866  cmpfii  23374  ptbasfi  23546  fbssint  23803  shintcl  31401  chintcl  31403  zarcmplem  34025  inelpisys  34298  rankeq1o  36353  bj-0int  37413  bj-ismoored  37419  bj-snmoore  37425  bj-prmoore  37427  neificl  38074  heibor1lem  38130  elrfi  43126  elrfirn  43127