Theorem inteq 4848

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

Syntax hints:   → wi 4   = wceq 1543  {cab 2714  ∀wral 3051  ∩ cint 4845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-ral 3056  df-int 4846

This theorem is referenced by:  inteqi  4849  inteqd  4850  unissint  4869  uniintsn  4884  rint0  4887  intex  5215  intnex  5216  elreldm  5789  elxp5  7679  1stval2  7756  oev2  8228  fundmen  8686  xpsnen  8707  fiint  8926  elfir  9009  inelfi  9012  fiin  9016  cardmin2  9580  isfin2-2  9898  incexclem  15363  mreintcl  17052  ismred2  17060  fiinopn  21752  cmpfii  22260  ptbasfi  22432  fbssint  22689  shintcl  29365  chintcl  29367  zarcmplem  31499  inelpisys  31788  rankeq1o  34159  bj-0int  34956  bj-ismoored  34962  bj-snmoore  34968  bj-prmoore  34970  neificl  35597  heibor1lem  35653  elrfi  40160  elrfirn  40161