Theorem ineq12i 4117

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

This proof depends on syntax axioms:   = wceq 1569   ∩ cin 4091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-in 4093

This theorem is used by:  undir  4234  difundi  4237  difindir  4240  inrab  4263  inrab2  4264  elneldisj  4344  dfif4  4500  dfif5  4501  resindi  5990  resindir  5991  rninOLD  6143  inimass  6150  cnvrescnv  6193  predin  6336  funtp  6605  orduniss2  7851  offres  8002  fodomr  9158  fodomfir  9330  epinid0  9609  cnvepnep  9619  wemapwe  9708  cotr3  15143  explecnv  16046  psssdm2  18767  ablfacrp  20294  cnfldfunALT  21705  pjfval2  22027  ofco2  22778  iundisj2  25882  clwwlknondisj  30714  lejdiri  32153  cmbr3i  32214  nonbooli  32265  5oai  32275  3oalem5  32280  mayetes3i  32343  mdexchi  32949  disjpreima  33232  disjxpin  33236  iundisj2f  33238  xppreima  33293  iundisj2fi  33442  xpinpreima  34591  xpinpreima2  34592  ordtcnvNEW  34605  pprodcnveq  36772  dfiota3  36812  bj-inrab  37967  ptrest  38677  ftc1anclem6  38756  dmxrn  39459  xrnres3  39499  br2coss  39600  1cosscnvxrn  39637  refsymrels2  39721  dfeqvrels2  39744  dfeldisj5  39885  dnwech  44195  fgraphopab  44345  onfrALTlem5  45664  onfrALTlem4  45665  onfrALTlem5VD  46006  onfrALTlem4VD  46007  disjxp1  46225  disjinfi  46346  oppczeroo  50498