Theorem inteq 4893

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

Syntax hints:   → wi 4   = wceq 1542  {cab 2715  ∀wral 3052  ∩ cint 4890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ral 3053  df-rex 3063  df-int 4891

This theorem is referenced by:  inteqi  4894  inteqd  4895  unissint  4915  uniintsn  4928  rint0  4931  intex  5281  intnex  5282  elreldm  5884  elxp5  7867  1stval2  7952  oev2  8451  fundmen  8971  xpsnen  8992  fiint  9230  elfir  9321  inelfi  9324  fiin  9328  cardmin2  9914  isfin2-2  10232  incexclem  15792  mreintcl  17548  ismred2  17556  fiinopn  22876  cmpfii  23384  ptbasfi  23556  fbssint  23813  shintcl  31416  chintcl  31418  zarcmplem  34041  inelpisys  34314  rankeq1o  36369  bj-0int  37429  bj-ismoored  37435  bj-snmoore  37441  bj-prmoore  37443  neificl  38088  heibor1lem  38144  elrfi  43140  elrfirn  43141