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

Theorem unieqi 3782
 Description: Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
unieqi.1
Assertion
Ref Expression
unieqi

Proof of Theorem unieqi
StepHypRef Expression
1 unieqi.1 . 2
2 unieq 3781 . 2
31, 2ax-mp 5 1
 Colors of variables: wff set class Syntax hints:   wceq 1335  cuni 3772 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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139 This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rex 2441  df-uni 3773 This theorem is referenced by:  elunirab  3785  unisn  3788  uniop  4215  unisuc  4373  unisucg  4374  univ  4435  dfiun3g  4842  op1sta  5066  op2nda  5069  dfdm2  5119  iotajust  5133  dfiota2  5135  cbviota  5139  sb8iota  5141  dffv4g  5464  funfvdm2f  5532  riotauni  5783  1st0  6089  2nd0  6090  unielxp  6119  brtpos0  6196  recsfval  6259  uniqs  6535  xpassen  6772  sup00  6943  suplocexprlemell  7627  uptx  12645
 Copyright terms: Public domain W3C validator