Theorem inteq 4879

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

Syntax hints:   → wi 4   = wceq 1539  {cab 2715  ∀wral 3063  ∩ cint 4876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-ral 3068  df-int 4877

This theorem is referenced by:  inteqi  4880  inteqd  4881  unissint  4900  uniintsn  4915  rint0  4918  intex  5256  intnex  5257  elreldm  5833  elxp5  7744  1stval2  7821  oev2  8315  fundmen  8775  xpsnen  8796  fiint  9021  elfir  9104  inelfi  9107  fiin  9111  cardmin2  9688  isfin2-2  10006  incexclem  15476  mreintcl  17221  ismred2  17229  fiinopn  21958  cmpfii  22468  ptbasfi  22640  fbssint  22897  shintcl  29593  chintcl  29595  zarcmplem  31733  inelpisys  32022  rankeq1o  34400  bj-0int  35199  bj-ismoored  35205  bj-snmoore  35211  bj-prmoore  35213  neificl  35838  heibor1lem  35894  elrfi  40432  elrfirn  40433