Theorem inteq 4954

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

Syntax hints:   → wi 4   = wceq 1537  {cab 2712  ∀wral 3059  ∩ cint 4951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-ral 3060  df-rex 3069  df-int 4952

This theorem is referenced by:  inteqi  4955  inteqd  4956  unissint  4977  uniintsn  4990  rint0  4993  intex  5350  intnex  5351  elreldm  5949  elxp5  7946  1stval2  8030  oev2  8560  fundmen  9070  xpsnen  9094  fiint  9364  fiintOLD  9365  elfir  9453  inelfi  9456  fiin  9460  cardmin2  10037  isfin2-2  10357  incexclem  15869  mreintcl  17640  ismred2  17648  fiinopn  22923  cmpfii  23433  ptbasfi  23605  fbssint  23862  shintcl  31359  chintcl  31361  zarcmplem  33842  inelpisys  34135  rankeq1o  36153  bj-0int  37084  bj-ismoored  37090  bj-snmoore  37096  bj-prmoore  37098  neificl  37740  heibor1lem  37796  elrfi  42682  elrfirn  42683