Theorem ineq12i 4164

Description: Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)

Hypotheses

Ref	Expression
ineq1i.1	⊢ 𝐴 = 𝐵
ineq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
ineq12i	⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)

Proof of Theorem ineq12i

Step	Hyp	Ref	Expression
1		ineq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		ineq12i.2	. 2 ⊢ 𝐶 = 𝐷
3		ineq12 4161	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
4	1, 2, 3	mp2an 705	1 ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)

This proof depends on syntax axioms:   = wceq 1570   ∩ cin 3898

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-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 3906

This theorem is used by:  undir  4233  difundi  4236  difindir  4239  inrab  4262  inrab2  4263  elneldisj  4342  dfif4  4498  dfif5  4499  resindi  5988  resindir  5989  rninOLD  6138  inimass  6146  cnvrescnv  6189  predin  6325  funtp  6591  orduniss2  7830  offres  7981  fodomr  9129  fodomfir  9300  epinid0  9580  cnvepnep  9590  wemapwe  9679  cotr3  15054  explecnv  15957  psssdm2  18672  ablfacrp  20198  cnfldfunALT  21603  pjfval2  21925  ofco2  22676  iundisj2  25780  clwwlknondisj  30584  lejdiri  32023  cmbr3i  32084  nonbooli  32135  5oai  32145  3oalem5  32150  mayetes3i  32213  mdexchi  32819  disjpreima  33060  disjxpin  33064  iundisj2f  33066  xppreima  33121  iundisj2fi  33271  xpinpreima  34419  xpinpreima2  34420  ordtcnvNEW  34433  pprodcnveq  36463  dfiota3  36503  bj-inrab  37674  ptrest  38371  ftc1anclem6  38450  dmxrn  39138  xrnres3  39178  br2coss  39279  1cosscnvxrn  39316  refsymrels2  39400  dfeqvrels2  39423  dfeldisj5  39564  dnwech  43892  fgraphopab  44047  onfrALTlem5  45368  onfrALTlem4  45369  onfrALTlem5VD  45710  onfrALTlem4VD  45711  disjxp1  45906  disjinfi  46027  oppczeroo  50166