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

Theorem uneq1 3610
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 2493 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
21orbi1d 707 . . 3  |-  ( A  =  B  ->  (
( x  e.  A  \/  x  e.  C
)  <->  ( x  e.  B  \/  x  e.  C ) ) )
3 elun 3603 . . 3  |-  ( x  e.  ( A  u.  C )  <->  ( x  e.  A  \/  x  e.  C ) )
4 elun 3603 . . 3  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
52, 3, 43bitr4g 291 . 2  |-  ( A  =  B  ->  (
x  e.  ( A  u.  C )  <->  x  e.  ( B  u.  C
) ) )
65eqrdv 2417 1  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 369    = wceq 1437    e. wcel 1867    u. cun 3431
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-un 3438
This theorem is referenced by:  uneq2  3611  uneq12  3612  uneq1i  3613  uneq1d  3616  unineq  3720  prprc1  4104  uniprg  4227  relresfld  5373  relcoi1OLD  5376  unexb  6596  oarec  7262  xpider  7433  ralxpmap  7520  undifixp  7557  unxpdom  7776  enp1ilem  7802  findcard2  7808  domunfican  7841  pwfilem  7865  fin1a2lem10  8828  incexclem  13861  lcmfunsnlem  14574  ramub1lem1  14944  ramub1  14946  mreexexlem3d  15504  mreexexlem4d  15505  ipodrsima  16363  mplsubglem  18599  mretopd  20045  iscldtop  20048  nconsubb  20375  plyval  23054  spanun  27074  difeq  28028  unelldsys  28860  isros  28870  unelros  28873  difelros  28874  rossros  28882  measun  28913  inelcarsg  29013  mrsubvrs  29989  nofulllem2  30418  altopthsn  30554  rankung  30759  poimirlem28  31716  islshp  32298  lshpset2N  32438  paddval  33116  nacsfix  35307  eldioph4b  35407  eldioph4i  35408  diophren  35409  compne  36478  fiiuncl  37096  founiiun0  37136  meadjun  37857
  Copyright terms: Public domain W3C validator