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

Theorem uneq1 3322
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 2344 . . . 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 3316 . . 3  |-  ( x  e.  ( A  u.  C )  <->  ( x  e.  A  \/  x  e.  C ) )
4 elun 3316 . . 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 2281 1  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357    = wceq 1623    e. wcel 1684    u. cun 3150
This theorem is referenced by:  uneq2  3323  uneq12  3324  uneq1i  3325  uneq1d  3328  unineq  3419  prprc1  3736  uniprg  3842  unexb  4520  relresfld  5199  relcoi1  5201  oarec  6560  xpider  6730  undifixp  6852  unxpdom  7070  enp1ilem  7092  findcard2  7098  domunfican  7129  pwfilem  7150  fin1a2lem10  8035  incexclem  12295  ramub1lem1  13073  ramub1  13075  mreexexlem3d  13548  mreexexlem4d  13549  ipodrsima  14268  mplsubglem  16179  mretopd  16829  iscldtop  16832  nconsubb  17149  plyval  19575  spanun  22124  difeq  23128  measxun  23539  nofulllem2  24357  brsuccf  24480  altopthsn  24495  rankung  24796  islimrs4  25582  hdrmp  25706  ralxpmap  26761  nacsfix  26787  eldioph4b  26894  eldioph4i  26895  diophren  26896  compne  27642  islshp  29169  lshpset2N  29309  paddval  29987
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157
  Copyright terms: Public domain W3C validator