Theorem ineq12i 4171

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 4168	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
4	1, 2, 3	mp2an 705	1 ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-in 3913

This theorem is used by:  undir  4240  difundi  4243  difindir  4246  inrab  4269  inrab2  4270  elneldisj  4349  dfif4  4505  dfif5  4506  resindi  5996  resindir  5997  rninOLD  6146  inimass  6154  cnvrescnv  6196  predin  6332  funtp  6597  orduniss2  7835  offres  7986  fodomr  9123  fodomfir  9294  epinid0  9574  cnvepnep  9584  wemapwe  9673  cotr3  15041  explecnv  15944  psssdm2  18661  ablfacrp  20184  cnfldfunALT  21589  pjfval2  21911  ofco2  22660  iundisj2  25761  clwwlknondisj  30531  lejdiri  31964  cmbr3i  32025  nonbooli  32076  5oai  32086  3oalem5  32091  mayetes3i  32154  mdexchi  32760  disjpreima  33002  disjxpin  33006  iundisj2f  33008  xppreima  33063  iundisj2fi  33214  xpinpreima  34362  xpinpreima2  34363  ordtcnvNEW  34376  pprodcnveq  36412  dfiota3  36452  bj-inrab  37622  ptrest  38329  ftc1anclem6  38408  dmxrn  39096  xrnres3  39136  br2coss  39237  1cosscnvxrn  39274  refsymrels2  39358  dfeqvrels2  39381  dfeldisj5  39522  dnwech  43835  fgraphopab  43990  onfrALTlem5  45311  onfrALTlem4  45312  onfrALTlem5VD  45653  onfrALTlem4VD  45654  disjxp1  45849  disjinfi  45970  oppczeroo  50074