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

Theorem uneq1 3572
Description: Equality theorem for the 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 2538 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
21orbi1d 717 . . 3  |-  ( A  =  B  ->  (
( x  e.  A  \/  x  e.  C
)  <->  ( x  e.  B  \/  x  e.  C ) ) )
3 elun 3565 . . 3  |-  ( x  e.  ( A  u.  C )  <->  ( x  e.  A  \/  x  e.  C ) )
4 elun 3565 . . 3  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
52, 3, 43bitr4g 296 . 2  |-  ( A  =  B  ->  (
x  e.  ( A  u.  C )  <->  x  e.  ( B  u.  C
) ) )
65eqrdv 2469 1  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 375    = wceq 1452    e. wcel 1904    u. cun 3388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-un 3395
This theorem is referenced by:  uneq2  3573  uneq12  3574  uneq1i  3575  uneq1d  3578  unineq  3684  prprc1  4073  uniprg  4204  relresfld  5369  relcoi1OLD  5372  unexb  6610  oarec  7281  xpider  7452  ralxpmap  7539  undifixp  7576  unxpdom  7797  enp1ilem  7823  findcard2  7829  domunfican  7862  pwfilem  7886  fin1a2lem10  8857  incexclem  13971  lcmfunsnlem  14693  ramub1lem1  15063  ramub1  15065  mreexexlem3d  15630  mreexexlem4d  15631  ipodrsima  16489  mplsubglem  18735  mretopd  20185  iscldtop  20188  nconsubb  20515  plyval  23226  spanun  27279  difeq  28230  unelldsys  29054  isros  29064  unelros  29067  difelros  29068  rossros  29076  measun  29107  inelcarsg  29216  mrsubvrs  30232  nofulllem2  30663  altopthsn  30799  rankung  31004  poimirlem28  32032  islshp  32616  lshpset2N  32756  paddval  33434  nacsfix  35625  eldioph4b  35725  eldioph4i  35726  diophren  35727  compne  36863  fiiuncl  37465  founiiun0  37536  meadjun  38416  hoidmvle  38540
  Copyright terms: Public domain W3C validator