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

Theorem ineq12i 3555
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  |-  A  =  B
ineq12i.2  |-  C  =  D
Assertion
Ref Expression
ineq12i  |-  ( A  i^i  C )  =  ( B  i^i  D
)

Proof of Theorem ineq12i
StepHypRef Expression
1 ineq1i.1 . 2  |-  A  =  B
2 ineq12i.2 . 2  |-  C  =  D
3 ineq12 3552 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
41, 2, 3mp2an 672 1  |-  ( A  i^i  C )  =  ( B  i^i  D
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    i^i cin 3332
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-in 3340
This theorem is referenced by:  undir  3604  difundi  3607  difindir  3610  inrab  3627  inrab2  3628  dfif4  3809  dfif5  3810  inxp  4977  resindi  5131  resindir  5132  rnin  5251  inimass  5258  funtp  5475  orduniss2  6449  offres  6577  fodomr  7467  wemapwe  7933  wemapweOLD  7934  explecnv  13332  psssdm2  15390  ablfacrp  16572  pjfval2  18139  ofco2  18337  iundisj2  21035  lejdiri  24947  cmbr3i  25008  nonbooli  25059  5oai  25069  3oalem5  25074  mayetes3i  25138  mdexchi  25744  disjpreima  25933  disjxpin  25935  iundisj2f  25937  xppreima  25969  iundisj2fi  26086  xpinpreima  26341  xpinpreima2  26342  ordtcnvNEW  26355  predin  27655  pprodcnveq  27919  dfiota3  27959  ptrest  28430  ftc1anclem6  28477  dnwech  29406  fgraphopab  29583  onfrALTlem5  31255  onfrALTlem4  31256  onfrALTlem5VD  31626  onfrALTlem4VD  31627  bj-inrab  32435
  Copyright terms: Public domain W3C validator