ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  uneq2d Unicode version

Theorem uneq2d 3304
Description: Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)
Hypothesis
Ref Expression
uneq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
uneq2d  |-  ( ph  ->  ( C  u.  A
)  =  ( C  u.  B ) )

Proof of Theorem uneq2d
StepHypRef Expression
1 uneq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 uneq2 3298 . 2  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
31, 2syl 14 1  |-  ( ph  ->  ( C  u.  A
)  =  ( C  u.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1364    u. cun 3142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148
This theorem is referenced by:  ifeq2  3553  tpeq3  3695  iununir  3985  unisucg  4429  relcoi1  5175  resasplitss  5410  fvun1  5598  fmptapd  5723  fvunsng  5726  fnsnsplitss  5731  tfr1onlemaccex  6367  tfrcllemaccex  6380  rdgeq1  6390  rdgivallem  6400  rdgisuc1  6403  rdgon  6405  rdg0  6406  oav2  6482  oasuc  6483  omv2  6484  omsuc  6491  fnsnsplitdc  6524  unsnfidcex  6937  undifdc  6941  fiintim  6946  ssfirab  6951  fnfi  6954  fidcenumlemr  6972  sbthlemi5  6978  sbthlemi6  6979  pm54.43  7207  fzsuc  10087  fseq1p1m1  10112  fseq1m1p1  10113  fzosplitsnm1  10227  fzosplitsn  10251  fzosplitprm1  10252  resunimafz0  10829  zfz1isolemsplit  10836  fsumm1  11442  fprodm1  11624  ennnfonelemp1  12425  ennnfonelemhdmp1  12428  ennnfonelemkh  12431  ennnfonelemhf1o  12432  ennnfonelemnn0  12441  strsetsid  12513  setscom  12520  lspun0  13702  bj-charfundcALT  14945
  Copyright terms: Public domain W3C validator