Theorem inteq 4887

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

Syntax hints:   → wi 4   = wceq 1547  {cab 2718  ∀wral 3054  ∩ cint 4884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-ral 3055  df-rex 3065  df-int 4885

This theorem is referenced by:  inteqi  4888  inteqd  4889  unissint  4909  uniintsn  4922  rint0  4925  intex  5279  intnex  5280  elreldm  5884  elxp5  7870  1stval2  7955  oev2  8455  fundmen  8975  xpsnen  8996  fiint  9234  elfir  9325  inelfi  9328  fiin  9332  cardmin2  9921  isfin2-2  10239  incexclem  15799  mreintcl  17555  ismred2  17563  fiinopn  22891  cmpfii  23399  ptbasfi  23571  fbssint  23828  shintcl  31426  chintcl  31428  zarcmplem  34072  inelpisys  34345  rankeq1o  36406  bj-0int  37466  bj-ismoored  37472  bj-snmoore  37478  bj-prmoore  37480  neificl  38127  heibor1lem  38183  elrfi  43150  elrfirn  43151