Theorem inteq 4930

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

Syntax hints:   → wi 4   = wceq 1540  {cab 2714  ∀wral 3052  ∩ cint 4927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-ral 3053  df-rex 3062  df-int 4928

This theorem is referenced by:  inteqi  4931  inteqd  4932  unissint  4953  uniintsn  4966  rint0  4969  intex  5319  intnex  5320  elreldm  5920  elxp5  7924  1stval2  8010  oev2  8540  fundmen  9050  xpsnen  9074  fiint  9343  fiintOLD  9344  elfir  9432  inelfi  9435  fiin  9439  cardmin2  10018  isfin2-2  10338  incexclem  15857  mreintcl  17612  ismred2  17620  fiinopn  22844  cmpfii  23352  ptbasfi  23524  fbssint  23781  shintcl  31316  chintcl  31318  zarcmplem  33917  inelpisys  34190  rankeq1o  36194  bj-0int  37124  bj-ismoored  37130  bj-snmoore  37136  bj-prmoore  37138  neificl  37782  heibor1lem  37838  elrfi  42684  elrfirn  42685