Theorem inteq 4916

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

Syntax hints:   → wi 4   = wceq 1570  {cab 2741  ∀wral 3079  ∩ cint 4913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-ral 3080  df-rex 3090  df-int 4914

This theorem is referenced by:  inteqi  4917  inteqd  4918  unissint  4938  uniintsn  4951  rint0  4954  intex  5316  intnex  5317  elreldm  5927  elxp5  7921  1stval2  8004  oev2  8509  fundmen  9029  xpsnen  9050  fiint  9287  elfir  9376  inelfi  9379  fiin  9383  cardmin2  9986  isfin2-2  10304  incexclem  15892  mreintcl  17648  ismred2  17656  fiinopn  23039  cmpfii  23547  ptbasfi  23719  fbssint  23976  shintcl  31660  chintcl  31662  zarcmplem  34249  inelpisys  34522  rankeq1o  36641  bj-0int  37721  bj-ismoored  37727  bj-snmoore  37733  bj-prmoore  37735  neificl  38382  heibor1lem  38438  elrfi  43405  elrfirn  43406