Theorem inteq 4878

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

Syntax hints:   → wi 4   = wceq 1533  {cab 2799  ∀wral 3138  ∩ cint 4875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-int 4876

This theorem is referenced by:  inteqi  4879  inteqd  4880  unissint  4899  uniintsn  4912  rint0  4915  intex  5239  intnex  5240  elreldm  5804  elxp5  7627  1stval2  7705  oev2  8147  fundmen  8582  xpsnen  8600  fiint  8794  elfir  8878  inelfi  8881  fiin  8885  cardmin2  9426  isfin2-2  9740  incexclem  15190  mreintcl  16865  ismred2  16873  fiinopn  21508  cmpfii  22016  ptbasfi  22188  fbssint  22445  shintcl  29106  chintcl  29108  inelpisys  31413  rankeq1o  33632  bj-0int  34392  bj-ismoored  34398  bj-snmoore  34404  bj-prmoore  34406  neificl  35027  heibor1lem  35086  elrfi  39289  elrfirn  39290