Theorem inteq 4907

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

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

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 4905

This theorem is referenced by:  inteqi  4908  inteqd  4909  unissint  4929  uniintsn  4942  rint0  4945  intex  5291  intnex  5292  elreldm  5892  elxp5  7875  1stval2  7960  oev2  8460  fundmen  8980  xpsnen  9001  fiint  9239  elfir  9330  inelfi  9333  fiin  9337  cardmin2  9923  isfin2-2  10241  incexclem  15771  mreintcl  17526  ismred2  17534  fiinopn  22857  cmpfii  23365  ptbasfi  23537  fbssint  23794  shintcl  31417  chintcl  31419  zarcmplem  34058  inelpisys  34331  rankeq1o  36384  bj-0int  37348  bj-ismoored  37354  bj-snmoore  37360  bj-prmoore  37362  neificl  37998  heibor1lem  38054  elrfi  43045  elrfirn  43046