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

Theorem unieqd 3715
Description: Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)
Hypothesis
Ref Expression
unieqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
unieqd  |-  ( ph  ->  U. A  =  U. B )

Proof of Theorem unieqd
StepHypRef Expression
1 unieqd.1 . 2  |-  ( ph  ->  A  =  B )
2 unieq 3713 . 2  |-  ( A  =  B  ->  U. A  =  U. B )
31, 2syl 14 1  |-  ( ph  ->  U. A  =  U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1314   U.cuni 3704
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-rex 2397  df-uni 3705
This theorem is referenced by:  uniprg  3719  unisng  3721  unisn3  4334  onsucuni2  4447  opswapg  4993  elxp4  4994  elxp5  4995  iotaeq  5064  iotabi  5065  uniabio  5066  funfvdm  5450  funfvdm2  5451  fvun1  5453  fniunfv  5629  funiunfvdm  5630  1stvalg  6006  2ndvalg  6007  fo1st  6021  fo2nd  6022  f1stres  6023  f2ndres  6024  2nd1st  6044  cnvf1olem  6087  brtpos2  6114  dftpos4  6126  tpostpos  6127  recseq  6169  tfrexlem  6197  ixpsnf1o  6596  xpcomco  6686  xpassen  6690  xpdom2  6691  supeq1  6839  supeq2  6842  supeq3  6843  supeq123d  6844  en2other2  7016  dfinfre  8674  hashinfom  10475  hashennn  10477  fsumcnv  11157  isbasisg  12117  basis1  12120  baspartn  12123  tgval  12124  eltg  12127  ntrfval  12175  ntrval  12185  tgrest  12244  restuni2  12252  lmfval  12267  cnfval  12269  cnpfval  12270  txtopon  12337  txswaphmeolem  12395  peano4nninf  13034
  Copyright terms: Public domain W3C validator