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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  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  5986  resindir  5987  rninOLD  6138  inimass  6145  cnvrescnv  6188  predin  6330  funtp  6597  orduniss2  7844  offres  7995  fodomr  9147  fodomfir  9319  epinid0  9599  cnvepnep  9609  wemapwe  9698  cotr3  15131  explecnv  16034  psssdm2  18755  ablfacrp  20282  cnfldfunALT  21693  pjfval2  22015  ofco2  22766  iundisj2  25870  clwwlknondisj  30702  lejdiri  32141  cmbr3i  32202  nonbooli  32253  5oai  32263  3oalem5  32268  mayetes3i  32331  mdexchi  32937  disjpreima  33178  disjxpin  33182  iundisj2f  33184  xppreima  33239  iundisj2fi  33389  xpinpreima  34538  xpinpreima2  34539  ordtcnvNEW  34552  pprodcnveq  36645  dfiota3  36685  bj-inrab  37840  ptrest  38537  ftc1anclem6  38616  dmxrn  39319  xrnres3  39359  br2coss  39460  1cosscnvxrn  39497  refsymrels2  39581  dfeqvrels2  39604  dfeldisj5  39745  dnwech  44054  fgraphopab  44204  onfrALTlem5  45524  onfrALTlem4  45525  onfrALTlem5VD  45866  onfrALTlem4VD  45867  disjxp1  46085  disjinfi  46206  oppczeroo  50344