Theorem inteq 4911

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 2831	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} = {𝑥 ∣ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦})
3		dfint2 4910	. 2 ⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦}
4		dfint2 4910	. 2 ⊢ ∩ 𝐵 = {𝑥 ∣ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦}
5	2, 3, 4	3eqtr4g 2825	1 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)

Syntax hints:   → wi 4   = wceq 1563  {cab 2743  ∀wral 3079  ∩ cint 4908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-ral 3080  df-rex 3090  df-int 4909

This theorem is referenced by:  inteqi  4912  inteqd  4913  unissint  4933  uniintsn  4946  rint0  4949  intex  5305  intnex  5306  elreldm  5916  elxp5  7908  1stval2  7991  oev2  8496  fundmen  9016  xpsnen  9037  fiint  9274  elfir  9363  inelfi  9366  fiin  9370  cardmin2  9973  isfin2-2  10291  incexclem  15880  mreintcl  17637  ismred2  17645  fiinopn  23019  cmpfii  23527  ptbasfi  23699  fbssint  23956  shintcl  31591  chintcl  31593  zarcmplem  34188  inelpisys  34461  rankeq1o  36534  bj-0int  37603  bj-ismoored  37609  bj-snmoore  37615  bj-prmoore  37617  neificl  38264  heibor1lem  38320  elrfi  43287  elrfirn  43288