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

Theorem ineq12i 4022
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 4019 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3mp2an 675 1 (𝐴𝐶) = (𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  cin 3779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-in 3787
This theorem is referenced by:  undir  4089  difundi  4092  difindir  4095  inrab  4111  inrab2  4112  elneldisj  4172  elneldisjOLD  4174  dfif4  4305  dfif5  4306  inxp  5470  resindi  5630  resindir  5631  rnin  5767  inimass  5774  predin  5930  funtp  6167  orduniss2  7273  offres  7403  fodomr  8360  epinid0  8754  cnvepnep  8760  wemapwe  8851  cotr3  13962  explecnv  14839  psssdm2  17440  ablfacrp  18687  cnfldfun  19986  pjfval2  20284  ofco2  20489  iundisj2  23553  clwwlknondisj  27303  lejdiri  28749  cmbr3i  28810  nonbooli  28861  5oai  28871  3oalem5  28876  mayetes3i  28939  mdexchi  29545  disjpreima  29745  disjxpin  29749  iundisj2f  29751  xppreima  29799  iundisj2fi  29906  xpinpreima  30300  xpinpreima2  30301  ordtcnvNEW  30314  pprodcnveq  32333  dfiota3  32373  bj-inrab  33253  ptrest  33740  ftc1anclem6  33821  xrnres3  34494  br2coss  34525  1cosscnvxrn  34557  refsymrels2  34643  dnwech  38137  fgraphopab  38307  onfrALTlem5  39273  onfrALTlem4  39274  onfrALTlem5VD  39633  onfrALTlem4VD  39634  disjxp1  39749  disjinfi  39887
  Copyright terms: Public domain W3C validator