Theorem inteq 4915

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

Syntax hints:   → wi 4   = wceq 1541  {cab 2708  ∀wral 3060  ∩ cint 4912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-ral 3061  df-int 4913

This theorem is referenced by:  inteqi  4916  inteqd  4917  unissint  4938  uniintsn  4953  rint0  4956  intex  5299  intnex  5300  elreldm  5895  elxp5  7865  1stval2  7943  oev2  8474  fundmen  8982  xpsnen  9006  fiint  9275  elfir  9360  inelfi  9363  fiin  9367  cardmin2  9944  isfin2-2  10264  incexclem  15732  mreintcl  17489  ismred2  17497  fiinopn  22287  cmpfii  22797  ptbasfi  22969  fbssint  23226  shintcl  30335  chintcl  30337  zarcmplem  32551  inelpisys  32842  rankeq1o  34832  bj-0int  35645  bj-ismoored  35651  bj-snmoore  35657  bj-prmoore  35659  neificl  36285  heibor1lem  36341  elrfi  41075  elrfirn  41076