Theorem inteq 4900

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

Syntax hints:   → wi 4   = wceq 1541  {cab 2709  ∀wral 3047  ∩ cint 4897

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 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-ral 3048  df-rex 3057  df-int 4898

This theorem is referenced by:  inteqi  4901  inteqd  4902  unissint  4922  uniintsn  4935  rint0  4938  intex  5282  intnex  5283  elreldm  5875  elxp5  7853  1stval2  7938  oev2  8438  fundmen  8953  xpsnen  8974  fiint  9211  elfir  9299  inelfi  9302  fiin  9306  cardmin2  9889  isfin2-2  10207  incexclem  15740  mreintcl  17494  ismred2  17502  fiinopn  22814  cmpfii  23322  ptbasfi  23494  fbssint  23751  shintcl  31305  chintcl  31307  zarcmplem  33889  inelpisys  34162  rankeq1o  36204  bj-0int  37134  bj-ismoored  37140  bj-snmoore  37146  bj-prmoore  37148  neificl  37792  heibor1lem  37848  elrfi  42726  elrfirn  42727