Theorem inteq 4902

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 3291	. . 3 ⊢ (𝐴 = 𝐵 → (∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦))
2	1	abbidv 2799	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} = {𝑥 ∣ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦})
3		dfint2 4901	. 2 ⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦}
4		dfint2 4901	. 2 ⊢ ∩ 𝐵 = {𝑥 ∣ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦}
5	2, 3, 4	3eqtr4g 2793	1 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)

Syntax hints:   → wi 4   = wceq 1541  {cab 2711  ∀wral 3049  ∩ cint 4899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-ral 3050  df-rex 3059  df-int 4900

This theorem is referenced by:  inteqi  4903  inteqd  4904  unissint  4924  uniintsn  4937  rint0  4940  intex  5286  intnex  5287  elreldm  5882  elxp5  7862  1stval2  7947  oev2  8447  fundmen  8963  xpsnen  8984  fiint  9221  elfir  9309  inelfi  9312  fiin  9316  cardmin2  9902  isfin2-2  10220  incexclem  15753  mreintcl  17507  ismred2  17515  fiinopn  22826  cmpfii  23334  ptbasfi  23506  fbssint  23763  shintcl  31321  chintcl  31323  zarcmplem  33905  inelpisys  34178  rankeq1o  36226  bj-0int  37156  bj-ismoored  37162  bj-snmoore  37168  bj-prmoore  37170  neificl  37803  heibor1lem  37859  elrfi  42801  elrfirn  42802