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

Syntax hints:   → wi 4   = wceq 1541  {cab 2711  ∀wral 3048  ∩ 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 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 3049  df-rex 3058  df-int 4898

This theorem is referenced by:  inteqi  4901  inteqd  4902  unissint  4922  uniintsn  4935  rint0  4938  intex  5284  intnex  5285  elreldm  5879  elxp5  7859  1stval2  7944  oev2  8444  fundmen  8960  xpsnen  8981  fiint  9218  elfir  9306  inelfi  9309  fiin  9313  cardmin2  9899  isfin2-2  10217  incexclem  15745  mreintcl  17499  ismred2  17507  fiinopn  22817  cmpfii  23325  ptbasfi  23497  fbssint  23754  shintcl  31312  chintcl  31314  zarcmplem  33915  inelpisys  34188  rankeq1o  36236  bj-0int  37166  bj-ismoored  37172  bj-snmoore  37178  bj-prmoore  37180  neificl  37814  heibor1lem  37870  elrfi  42812  elrfirn  42813