Theorem inteq 4920

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {cab 2744  ∀wral 3082  ∩ cint 4917

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 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-ral 3083  df-rex 3093  df-int 4918

This theorem is used by:  inteqi  4921  inteqd  4922  unissint  4942  uniintsn  4955  rint0  4958  intex  5319  intnex  5320  elreldm  5930  elxp5  7929  1stval2  8012  oev2  8517  fundmen  9038  xpsnen  9059  fiint  9296  elfir  9385  inelfi  9388  fiin  9392  cardmin2  10004  isfin2-2  10321  incexclem  15916  mreintcl  17672  ismred2  17680  fiinopn  23095  cmpfii  23603  ptbasfi  23775  fbssint  24032  shintcl  31719  chintcl  31721  zarcmplem  34302  inelpisys  34576  rankeq1o  36684  bj-0int  37784  bj-ismoored  37790  bj-snmoore  37796  bj-prmoore  37798  neificl  38445  heibor1lem  38501  elrfi  43466  elrfirn  43467