NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  unieqi GIF version

Theorem unieqi 3901
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 A = B

Proof of Theorem unieqi
StepHypRef Expression
1 unieqi.1 . 2 A = B
2 unieq 3900 . 2 (A = BA = B)
31, 2ax-mp 5 1 A = B
Colors of variables: wff setvar class
Syntax hints:   = wceq 1642  cuni 3891
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-rex 2620  df-uni 3892
This theorem is referenced by:  elunirab  3904  unisn  3907  iotajust  4338  dfiota2  4340  cbviota  4344  sb8iota  4346  dfiota4  4372  op1sta  5072  opswap  5074  op2nda  5076  funfv2  5376  funfv2f  5377  fvco2  5382  funiunfv  5467  elunirn  5470  uniqs  5984
  Copyright terms: Public domain W3C validator