MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uneq1 Structured version   Unicode version

Theorem uneq1 3633
Description: Equality theorem for union of two classes. (Contributed by NM, 15-Jul-1993.)
Assertion
Ref Expression
uneq1  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )

Proof of Theorem uneq1
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eleq2 2514 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
21orbi1d 702 . . 3  |-  ( A  =  B  ->  (
( x  e.  A  \/  x  e.  C
)  <->  ( x  e.  B  \/  x  e.  C ) ) )
3 elun 3627 . . 3  |-  ( x  e.  ( A  u.  C )  <->  ( x  e.  A  \/  x  e.  C ) )
4 elun 3627 . . 3  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
52, 3, 43bitr4g 288 . 2  |-  ( A  =  B  ->  (
x  e.  ( A  u.  C )  <->  x  e.  ( B  u.  C
) ) )
65eqrdv 2438 1  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368    = wceq 1381    e. wcel 1802    u. cun 3456
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-un 3463
This theorem is referenced by:  uneq2  3634  uneq12  3635  uneq1i  3636  uneq1d  3639  unineq  3730  prprc1  4121  uniprg  4244  relresfld  5520  relcoi1  5522  unexb  6581  oarec  7209  xpider  7380  ralxpmap  7466  undifixp  7503  unxpdom  7725  enp1ilem  7752  findcard2  7758  domunfican  7791  pwfilem  7812  fin1a2lem10  8787  incexclem  13622  ramub1lem1  14416  ramub1  14418  mreexexlem3d  14915  mreexexlem4d  14916  ipodrsima  15664  mplsubglem  17961  mplsubglemOLD  17963  mretopd  19459  iscldtop  19462  nconsubb  19790  plyval  22456  spanun  26328  difeq  27281  measun  28048  mrsubvrs  28748  nofulllem2  29431  brsuccf  29559  altopthsn  29579  rankung  29791  nacsfix  30612  eldioph4b  30713  eldioph4i  30714  diophren  30715  compne  31296  islshp  34406  lshpset2N  34546  paddval  35224
  Copyright terms: Public domain W3C validator