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

Theorem uneq2d 3097
 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 3091 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1243   ∪ cun 2915 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-un 2922 This theorem is referenced by:  ifeq2  3335  tpeq3  3458  iununir  3738  unisucg  4151  relcoi1  4849  resasplitss  5069  fvun1  5239  fmptapd  5354  fvunsng  5357  rdgeq1  5958  rdgivallem  5968  rdgisuc1  5971  rdg0  5974  oav2  6043  oasuc  6044  omv2  6045  omsuc  6051  fzsuc  8931  fseq1p1m1  8956  fseq1m1p1  8957  fzosplitsnm1  9065  fzosplitsn  9089  fzosplitprm1  9090
 Copyright terms: Public domain W3C validator