MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ineq12i Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 ineq1i.1 . 2 𝐴 = 𝐵
2 ineq12i.2 . 2 𝐶 = 𝐷
3 ineq12 4168 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3mp2an 691 1 (𝐴𝐶) = (𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cin 3910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-in 3918
This theorem is referenced by:  undir  4237  difundi  4240  difindir  4243  inrab  4267  inrab2  4268  elneldisj  4349  dfif4  4502  dfif5  4503  inxp  5789  resindi  5954  resindir  5955  rnin  6100  inimass  6108  cnvrescnv  6148  predin  6282  funtp  6559  orduniss2  7769  offres  7917  fodomr  9075  epinid0  9541  cnvepnep  9549  wemapwe  9638  cotr3  14869  explecnv  15755  psssdm2  18475  ablfacrp  19850  cnfldfunALT  20825  cnfldfunALTOLD  20826  pjfval2  21131  ofco2  21816  iundisj2  24929  clwwlknondisj  29097  lejdiri  30523  cmbr3i  30584  nonbooli  30635  5oai  30645  3oalem5  30650  mayetes3i  30713  mdexchi  31319  disjpreima  31548  disjxpin  31552  iundisj2f  31554  xppreima  31608  iundisj2fi  31747  xpinpreima  32544  xpinpreima2  32545  ordtcnvNEW  32558  pprodcnveq  34514  dfiota3  34554  bj-inrab  35443  ptrest  36123  ftc1anclem6  36202  xrnres3  36912  br2coss  36946  1cosscnvxrn  36983  refsymrels2  37073  dfeqvrels2  37096  dfeldisj5  37229  dnwech  41418  fgraphopab  41580  onfrALTlem5  42912  onfrALTlem4  42913  onfrALTlem5VD  43255  onfrALTlem4VD  43256  disjxp1  43365  disjinfi  43500
  Copyright terms: Public domain W3C validator