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

Theorem uneq1 3644
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 2533 . . . 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 3638 . . 3  |-  ( x  e.  ( A  u.  C )  <->  ( x  e.  A  \/  x  e.  C ) )
4 elun 3638 . . 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 2457 1  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368    = wceq 1374    e. wcel 1762    u. cun 3467
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-un 3474
This theorem is referenced by:  uneq2  3645  uneq12  3646  uneq1i  3647  uneq1d  3650  unineq  3741  prprc1  4130  uniprg  4252  relresfld  5525  relcoi1  5527  unexb  6575  oarec  7201  xpider  7372  ralxpmap  7458  undifixp  7495  unxpdom  7717  enp1ilem  7743  findcard2  7749  domunfican  7782  pwfilem  7803  fin1a2lem10  8778  incexclem  13600  ramub1lem1  14392  ramub1  14394  mreexexlem3d  14890  mreexexlem4d  14891  ipodrsima  15641  mplsubglem  17857  mplsubglemOLD  17859  mretopd  19352  iscldtop  19355  nconsubb  19683  plyval  22318  spanun  26125  difeq  27076  measun  27808  nofulllem2  29026  brsuccf  29154  altopthsn  29174  rankung  29386  nacsfix  30235  eldioph4b  30336  eldioph4i  30337  diophren  30338  compne  30882  islshp  33651  lshpset2N  33791  paddval  34469
  Copyright terms: Public domain W3C validator