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

Syntax hints:   → wi 4   = wceq 1559  {cab 2739  ∀wral 3075  ∩ cint 4904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-ral 3076  df-rex 3086  df-int 4905

This theorem is referenced by:  inteqi  4908  inteqd  4909  unissint  4929  uniintsn  4942  rint0  4945  intex  5299  intnex  5300  elreldm  5909  elxp5  7900  1stval2  7983  oev2  8487  fundmen  9008  xpsnen  9029  fiint  9267  elfir  9358  inelfi  9361  fiin  9365  cardmin2  9954  isfin2-2  10273  incexclem  15849  mreintcl  17606  ismred2  17614  fiinopn  22941  cmpfii  23449  ptbasfi  23621  fbssint  23878  shintcl  31479  chintcl  31481  zarcmplem  34139  inelpisys  34412  rankeq1o  36485  bj-0int  37555  bj-ismoored  37561  bj-snmoore  37567  bj-prmoore  37569  neificl  38216  heibor1lem  38272  elrfi  43239  elrfirn  43240