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

Theorem uneq2d 3233
 Description: Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)
Hypothesis
Ref Expression
uneq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
uneq2d (𝜑 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem uneq2d
StepHypRef Expression
1 uneq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 uneq2 3227 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1332   ∪ cun 3072 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3078 This theorem is referenced by:  ifeq2  3481  tpeq3  3617  iununir  3902  unisucg  4342  relcoi1  5076  resasplitss  5308  fvun1  5493  fmptapd  5617  fvunsng  5620  fnsnsplitss  5625  tfr1onlemaccex  6251  tfrcllemaccex  6264  rdgeq1  6274  rdgivallem  6284  rdgisuc1  6287  rdgon  6289  rdg0  6290  oav2  6365  oasuc  6366  omv2  6367  omsuc  6374  fnsnsplitdc  6407  unsnfidcex  6814  undifdc  6818  fiintim  6823  ssfirab  6828  fnfi  6831  fidcenumlemr  6849  sbthlemi5  6855  sbthlemi6  6856  pm54.43  7061  fzsuc  9878  fseq1p1m1  9903  fseq1m1p1  9904  fzosplitsnm1  10015  fzosplitsn  10039  fzosplitprm1  10040  resunimafz0  10604  zfz1isolemsplit  10611  fsumm1  11215  ennnfonelemp1  11948  ennnfonelemhdmp1  11951  ennnfonelemkh  11954  ennnfonelemhf1o  11955  ennnfonelemnn0  11964  strsetsid  12024  setscom  12031
 Copyright terms: Public domain W3C validator