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

Syntax hints:   → wi 4   = wceq 1540  {cab 2707  ∀wral 3044  ∩ cint 4910

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-ral 3045  df-rex 3054  df-int 4911

This theorem is referenced by:  inteqi  4914  inteqd  4915  unissint  4936  uniintsn  4949  rint0  4952  intex  5299  intnex  5300  elreldm  5899  elxp5  7899  1stval2  7985  oev2  8487  fundmen  9002  xpsnen  9025  fiint  9277  fiintOLD  9278  elfir  9366  inelfi  9369  fiin  9373  cardmin2  9952  isfin2-2  10272  incexclem  15802  mreintcl  17556  ismred2  17564  fiinopn  22788  cmpfii  23296  ptbasfi  23468  fbssint  23725  shintcl  31259  chintcl  31261  zarcmplem  33871  inelpisys  34144  rankeq1o  36159  bj-0int  37089  bj-ismoored  37095  bj-snmoore  37101  bj-prmoore  37103  neificl  37747  heibor1lem  37803  elrfi  42682  elrfirn  42683