Theorem inteq 4913

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {cab 2740  ∀wral 3078  ∩ cint 4910

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-ral 3079  df-rex 3089  df-int 4911

This theorem is used by:  inteqi  4914  inteqd  4915  unissint  4935  uniintsn  4948  rint0  4951  intex  5312  intnex  5313  elreldm  5923  elxp5  7924  1stval2  8007  oev2  8514  fundmen  9042  xpsnen  9063  fiint  9300  elfir  9389  inelfi  9392  fiin  9396  cardmin2  10008  isfin2-2  10325  incexclem  15929  mreintcl  17685  ismred2  17693  fiinopn  23132  cmpfii  23640  ptbasfi  23813  fbssint  24070  shintcl  31819  chintcl  31821  zarcmplem  34399  inelpisys  34673  rankeq1o  36759  bj-0int  37859  bj-ismoored  37865  bj-snmoore  37871  bj-prmoore  37873  neificl  38511  heibor1lem  38567  elrfi  43547  elrfirn  43548