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

Theorem ineq12i 4107
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 4104 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3mp2an 688 1 (𝐴𝐶) = (𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1522  cin 3858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rab 3114  df-v 3439  df-in 3866
This theorem is referenced by:  undir  4173  difundi  4176  difindir  4179  inrab  4195  inrab2  4196  elneldisj  4262  dfif4  4396  dfif5  4397  inxp  5589  resindi  5750  resindir  5751  rnin  5881  inimass  5888  predin  6046  funtp  6281  orduniss2  7404  offres  7540  fodomr  8515  epinid0  8910  cnvepnep  8917  wemapwe  9006  cotr3  14172  explecnv  15053  psssdm2  17654  ablfacrp  18905  cnfldfun  20239  pjfval2  20535  ofco2  20744  iundisj2  23833  clwwlknondisj  27577  lejdiri  29007  cmbr3i  29068  nonbooli  29119  5oai  29129  3oalem5  29134  mayetes3i  29197  mdexchi  29803  disjpreima  30024  disjxpin  30028  iundisj2f  30030  xppreima  30084  iundisj2fi  30206  xpinpreima  30766  xpinpreima2  30767  ordtcnvNEW  30780  pprodcnveq  32954  dfiota3  32994  bj-inrab  33820  ptrest  34441  ftc1anclem6  34522  xrnres3  35202  br2coss  35233  1cosscnvxrn  35265  refsymrels2  35351  dfeqvrels2  35373  dfeldisj5  35504  dnwech  39152  fgraphopab  39314  onfrALTlem5  40434  onfrALTlem4  40435  onfrALTlem5VD  40777  onfrALTlem4VD  40778  disjxp1  40889  disjinfi  41013
  Copyright terms: Public domain W3C validator