Theorem inteq 4948

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

Syntax hints:   → wi 4   = wceq 1539  {cab 2713  ∀wral 3060  ∩ cint 4945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-ral 3061  df-rex 3070  df-int 4946

This theorem is referenced by:  inteqi  4949  inteqd  4950  unissint  4971  uniintsn  4984  rint0  4987  intex  5343  intnex  5344  elreldm  5945  elxp5  7946  1stval2  8032  oev2  8562  fundmen  9072  xpsnen  9096  fiint  9367  fiintOLD  9368  elfir  9456  inelfi  9459  fiin  9463  cardmin2  10040  isfin2-2  10360  incexclem  15873  mreintcl  17639  ismred2  17647  fiinopn  22908  cmpfii  23418  ptbasfi  23590  fbssint  23847  shintcl  31350  chintcl  31352  zarcmplem  33881  inelpisys  34156  rankeq1o  36173  bj-0int  37103  bj-ismoored  37109  bj-snmoore  37115  bj-prmoore  37117  neificl  37761  heibor1lem  37817  elrfi  42710  elrfirn  42711