Theorem inteq 4905

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-ral 3052  df-rex 3061  df-int 4903

This theorem is referenced by:  inteqi  4906  inteqd  4907  unissint  4927  uniintsn  4940  rint0  4943  intex  5289  intnex  5290  elreldm  5884  elxp5  7865  1stval2  7950  oev2  8450  fundmen  8968  xpsnen  8989  fiint  9227  elfir  9318  inelfi  9321  fiin  9325  cardmin2  9911  isfin2-2  10229  incexclem  15759  mreintcl  17514  ismred2  17522  fiinopn  22845  cmpfii  23353  ptbasfi  23525  fbssint  23782  shintcl  31405  chintcl  31407  zarcmplem  34038  inelpisys  34311  rankeq1o  36365  bj-0int  37302  bj-ismoored  37308  bj-snmoore  37314  bj-prmoore  37316  neificl  37950  heibor1lem  38006  elrfi  42932  elrfirn  42933