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

Theorem unieqi 3819
Description: Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
unieqi.1  |-  A  =  B
Assertion
Ref Expression
unieqi  |-  U. A  =  U. B

Proof of Theorem unieqi
StepHypRef Expression
1 unieqi.1 . 2  |-  A  =  B
2 unieq 3818 . 2  |-  ( A  =  B  ->  U. A  =  U. B )
31, 2ax-mp 5 1  |-  U. A  =  U. B
Colors of variables: wff set class
Syntax hints:    = wceq 1353   U.cuni 3809
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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-uni 3810
This theorem is referenced by:  elunirab  3822  unisn  3825  uniop  4255  unisuc  4413  unisucg  4414  univ  4476  dfiun3g  4884  op1sta  5110  op2nda  5113  dfdm2  5163  iotajust  5177  dfiota2  5179  cbviota  5183  sb8iota  5185  dffv4g  5512  funfvdm2f  5581  riotauni  5836  1st0  6144  2nd0  6145  unielxp  6174  brtpos0  6252  recsfval  6315  uniqs  6592  xpassen  6829  sup00  7001  suplocexprlemell  7711  uptx  13744
  Copyright terms: Public domain W3C validator