Theorem inteq 4789

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

Syntax hints:   → wi 4   = wceq 1522  {cab 2775  ∀wral 3105  ∩ cint 4786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-ral 3110  df-int 4787

This theorem is referenced by:  inteqi  4790  inteqd  4791  unissint  4810  uniintsn  4823  rint0  4826  intex  5136  intnex  5137  elreldm  5692  elxp5  7489  1stval2  7567  oev2  8004  fundmen  8436  xpsnen  8453  fiint  8646  elfir  8730  inelfi  8733  fiin  8737  cardmin2  9278  isfin2-2  9592  incexclem  15029  mreintcl  16700  ismred2  16708  fiinopn  21198  cmpfii  21706  ptbasfi  21878  fbssint  22135  shintcl  28803  chintcl  28805  inelpisys  31035  rankeq1o  33248  bj-0int  34018  bj-ismoored  34025  bj-snmoore  34031  neificl  34586  heibor1lem  34645  elrfi  38802  elrfirn  38803