Theorem ineq12i 4198

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

Syntax hints:   = wceq 1540   ∩ cin 3930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-in 3938

This theorem is referenced by:  undir  4267  difundi  4270  difindir  4273  inrab  4296  inrab2  4297  elneldisj  4372  dfif4  4521  dfif5  4522  inxpOLD  5817  resindi  5987  resindir  5988  rnin  6140  inimass  6149  cnvrescnv  6189  predin  6321  funtp  6598  orduniss2  7832  offres  7987  fodomr  9147  fodomfir  9345  epinid0  9619  cnvepnep  9627  wemapwe  9716  cotr3  15002  explecnv  15886  psssdm2  18596  ablfacrp  20054  cnfldfunALT  21335  cnfldfunALTOLD  21348  pjfval2  21674  ofco2  22394  iundisj2  25507  clwwlknondisj  30097  lejdiri  31525  cmbr3i  31586  nonbooli  31637  5oai  31647  3oalem5  31652  mayetes3i  31715  mdexchi  32321  disjpreima  32570  disjxpin  32574  iundisj2f  32576  xppreima  32628  iundisj2fi  32779  xpinpreima  33942  xpinpreima2  33943  ordtcnvNEW  33956  pprodcnveq  35906  dfiota3  35946  bj-inrab  36950  ptrest  37648  ftc1anclem6  37727  xrnres3  38427  br2coss  38461  1cosscnvxrn  38498  refsymrels2  38588  dfeqvrels2  38611  dfeldisj5  38744  dnwech  43039  fgraphopab  43194  onfrALTlem5  44534  onfrALTlem4  44535  onfrALTlem5VD  44876  onfrALTlem4VD  44877  disjxp1  45060  disjinfi  45183  oppczeroo  49121