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

Theorem uneq1 3335
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 2357 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
21orbi1d 683 . . 3  |-  ( A  =  B  ->  (
( x  e.  A  \/  x  e.  C
)  <->  ( x  e.  B  \/  x  e.  C ) ) )
3 elun 3329 . . 3  |-  ( x  e.  ( A  u.  C )  <->  ( x  e.  A  \/  x  e.  C ) )
4 elun 3329 . . 3  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
52, 3, 43bitr4g 279 . 2  |-  ( A  =  B  ->  (
x  e.  ( A  u.  C )  <->  x  e.  ( B  u.  C
) ) )
65eqrdv 2294 1  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357    = wceq 1632    e. wcel 1696    u. cun 3163
This theorem is referenced by:  uneq2  3336  uneq12  3337  uneq1i  3338  uneq1d  3341  unineq  3432  prprc1  3749  uniprg  3858  unexb  4536  relresfld  5215  relcoi1  5217  oarec  6576  xpider  6746  undifixp  6868  unxpdom  7086  enp1ilem  7108  findcard2  7114  domunfican  7145  pwfilem  7166  fin1a2lem10  8051  incexclem  12311  ramub1lem1  13089  ramub1  13091  mreexexlem3d  13564  mreexexlem4d  13565  ipodrsima  14284  mplsubglem  16195  mretopd  16845  iscldtop  16848  nconsubb  17165  plyval  19591  spanun  22140  difeq  23144  measxun  23554  nofulllem2  24428  brsuccf  24551  altopthsn  24567  rankung  24868  islimrs4  25685  hdrmp  25809  ralxpmap  26864  nacsfix  26890  eldioph4b  26997  eldioph4i  26998  diophren  26999  compne  27745  islshp  29791  lshpset2N  29931  paddval  30609
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170
  Copyright terms: Public domain W3C validator