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

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

Proof of Theorem uneq2d
StepHypRef Expression
1 uneq1d.1 . 2 (φA = B)
2 uneq2 3064 . 2 (A = B → (𝐶A) = (𝐶B))
31, 2syl 14 1 (φ → (𝐶A) = (𝐶B))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1226  cun 2888
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 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-v 2533  df-un 2895
This theorem is referenced by:  ifeq2  3310  tpeq3  3428  iununir  3708  unisucg  4096  relcoi1  4772  resasplitss  4990  fvun1  5160  fmptapd  5275  fvunsng  5278  rdgeq1  5875  rdgi0g  5882  rdgivallem  5884  rdgisuc1  5887  rdg0  5891  oav2  5954  oasuc  5955  omv2  5956  omsuc  5962
  Copyright terms: Public domain W3C validator