Theorem inteq 4954

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

Syntax hints:   → wi 4   = wceq 1542  {cab 2710  ∀wral 3062  ∩ cint 4951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-ral 3063  df-rex 3072  df-int 4952

This theorem is referenced by:  inteqi  4955  inteqd  4956  unissint  4977  uniintsn  4992  rint0  4995  intex  5338  intnex  5339  elreldm  5935  elxp5  7914  1stval2  7992  oev2  8523  fundmen  9031  xpsnen  9055  fiint  9324  elfir  9410  inelfi  9413  fiin  9417  cardmin2  9994  isfin2-2  10314  incexclem  15782  mreintcl  17539  ismred2  17547  fiinopn  22403  cmpfii  22913  ptbasfi  23085  fbssint  23342  shintcl  30583  chintcl  30585  zarcmplem  32861  inelpisys  33152  rankeq1o  35143  bj-0int  35982  bj-ismoored  35988  bj-snmoore  35994  bj-prmoore  35996  neificl  36621  heibor1lem  36677  elrfi  41432  elrfirn  41433