Theorem inteq 4913

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {cab 2741  ∀wral 3080  ∩ cint 4910

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-ral 3081  df-rex 3091  df-int 4911

This theorem is used by:  inteqi  4914  inteqd  4915  unissint  4935  uniintsn  4948  rint0  4951  intex  5310  intnex  5311  elreldm  5925  elxp5  7962  1stval2  8045  oev2  8562  fundmen  9090  xpsnen  9111  fiint  9349  elfir  9437  inelfi  9440  fiin  9444  cardmin2  10110  isfin2-2  10427  incexclem  16037  mreintcl  17797  ismred2  17805  fiinopn  23252  cmpfii  23760  ptbasfi  23933  fbssint  24190  shintcl  31965  chintcl  31967  zarcmplem  34596  inelpisys  34870  rankeq1o  37123  bj-0int  38226  bj-ismoored  38232  bj-snmoore  38238  bj-prmoore  38240  neificl  38890  heibor1lem  38946  elrfi  43909  elrfirn  43910