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

Theorem unieqd 3797
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 3795 . 2 (𝐴 = 𝐵 𝐴 = 𝐵)
31, 2syl 14 1 (𝜑 𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1342   cuni 3786
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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146
This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-rex 2448  df-uni 3787
This theorem is referenced by:  uniprg  3801  unisng  3803  unisn3  4420  onsucuni2  4538  opswapg  5087  elxp4  5088  elxp5  5089  iotaeq  5158  iotabi  5159  uniabio  5160  funfvdm  5546  funfvdm2  5547  fvun1  5549  fniunfv  5727  funiunfvdm  5728  1stvalg  6105  2ndvalg  6106  fo1st  6120  fo2nd  6121  f1stres  6122  f2ndres  6123  2nd1st  6143  cnvf1olem  6186  brtpos2  6213  dftpos4  6225  tpostpos  6226  recseq  6268  tfrexlem  6296  ixpsnf1o  6696  xpcomco  6786  xpassen  6790  xpdom2  6791  supeq1  6945  supeq2  6948  supeq3  6949  supeq123d  6950  en2other2  7146  dfinfre  8845  hashinfom  10685  hashennn  10687  fsumcnv  11372  fprodcnv  11560  isbasisg  12640  basis1  12643  baspartn  12646  tgval  12647  eltg  12650  ntrfval  12698  ntrval  12708  tgrest  12767  restuni2  12775  lmfval  12790  cnfval  12792  cnpfval  12793  txtopon  12860  txswaphmeolem  12918  peano4nninf  13779
  Copyright terms: Public domain W3C validator