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

Theorem unieqd 3832
Description: Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)
Hypothesis
Ref Expression
unieqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
unieqd (𝜑 𝐴 = 𝐵)

Proof of Theorem unieqd
StepHypRef Expression
1 unieqd.1 . 2 (𝜑𝐴 = 𝐵)
2 unieq 3830 . 2 (𝐴 = 𝐵 𝐴 = 𝐵)
31, 2syl 14 1 (𝜑 𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1363   cuni 3821
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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169
This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-rex 2471  df-uni 3822
This theorem is referenced by:  uniprg  3836  unisng  3838  unisn3  4457  onsucuni2  4575  opswapg  5127  elxp4  5128  elxp5  5129  iotaeq  5198  iotabi  5199  uniabio  5200  funfvdm  5592  funfvdm2  5593  fvun1  5595  fniunfv  5776  funiunfvdm  5777  1stvalg  6157  2ndvalg  6158  fo1st  6172  fo2nd  6173  f1stres  6174  f2ndres  6175  2nd1st  6195  cnvf1olem  6239  brtpos2  6266  dftpos4  6278  tpostpos  6279  recseq  6321  tfrexlem  6349  ixpsnf1o  6750  xpcomco  6840  xpassen  6844  xpdom2  6845  supeq1  6999  supeq2  7002  supeq3  7003  supeq123d  7004  en2other2  7209  dfinfre  8927  hashinfom  10772  hashennn  10774  fsumcnv  11459  fprodcnv  11647  tgval  12729  ptex  12731  lssuni  13552  lspuni0  13613  lss0v  13619  isbasisg  13840  basis1  13843  baspartn  13846  eltg  13848  ntrfval  13896  ntrval  13906  tgrest  13965  restuni2  13973  lmfval  13988  cnfval  13990  cnpfval  13991  txtopon  14058  txswaphmeolem  14116  peano4nninf  15052
  Copyright terms: Public domain W3C validator