Theorem inteq 4882

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

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

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-ral 3069  df-int 4880

This theorem is referenced by:  inteqi  4883  inteqd  4884  unissint  4903  uniintsn  4918  rint0  4921  intex  5261  intnex  5262  elreldm  5844  elxp5  7770  1stval2  7848  oev2  8353  fundmen  8821  xpsnen  8842  fiint  9091  elfir  9174  inelfi  9177  fiin  9181  cardmin2  9757  isfin2-2  10075  incexclem  15548  mreintcl  17304  ismred2  17312  fiinopn  22050  cmpfii  22560  ptbasfi  22732  fbssint  22989  shintcl  29692  chintcl  29694  zarcmplem  31831  inelpisys  32122  rankeq1o  34473  bj-0int  35272  bj-ismoored  35278  bj-snmoore  35284  bj-prmoore  35286  neificl  35911  heibor1lem  35967  elrfi  40516  elrfirn  40517