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

Theorem uneq1 3431
Description: Equality theorem for union of two classes. (Contributed by NM, 5-Aug-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 2442 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
21orbi1d 684 . . 3  |-  ( A  =  B  ->  (
( x  e.  A  \/  x  e.  C
)  <->  ( x  e.  B  \/  x  e.  C ) ) )
3 elun 3425 . . 3  |-  ( x  e.  ( A  u.  C )  <->  ( x  e.  A  \/  x  e.  C ) )
4 elun 3425 . . 3  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
52, 3, 43bitr4g 280 . 2  |-  ( A  =  B  ->  (
x  e.  ( A  u.  C )  <->  x  e.  ( B  u.  C
) ) )
65eqrdv 2379 1  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358    = wceq 1649    e. wcel 1717    u. cun 3255
This theorem is referenced by:  uneq2  3432  uneq12  3433  uneq1i  3434  uneq1d  3437  unineq  3528  prprc1  3851  uniprg  3966  unexb  4643  relresfld  5330  relcoi1  5332  oarec  6735  xpider  6905  undifixp  7028  unxpdom  7246  enp1ilem  7272  findcard2  7278  domunfican  7309  pwfilem  7330  fin1a2lem10  8216  incexclem  12537  ramub1lem1  13315  ramub1  13317  mreexexlem3d  13792  mreexexlem4d  13793  ipodrsima  14512  mplsubglem  16419  mretopd  17073  iscldtop  17076  nconsubb  17401  plyval  19973  spanun  22889  difeq  23836  measun  24353  nofulllem2  25375  brsuccf  25498  altopthsn  25514  rankung  25815  ralxpmap  26427  nacsfix  26451  eldioph4b  26557  eldioph4i  26558  diophren  26559  compne  27305  islshp  29146  lshpset2N  29286  paddval  29964
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2362
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2506  df-v 2895  df-un 3262
  Copyright terms: Public domain W3C validator