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

Theorem uneq1 3496
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 2499 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
21orbi1d 685 . . 3  |-  ( A  =  B  ->  (
( x  e.  A  \/  x  e.  C
)  <->  ( x  e.  B  \/  x  e.  C ) ) )
3 elun 3490 . . 3  |-  ( x  e.  ( A  u.  C )  <->  ( x  e.  A  \/  x  e.  C ) )
4 elun 3490 . . 3  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
52, 3, 43bitr4g 281 . 2  |-  ( A  =  B  ->  (
x  e.  ( A  u.  C )  <->  x  e.  ( B  u.  C
) ) )
65eqrdv 2436 1  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 359    = wceq 1653    e. wcel 1726    u. cun 3320
This theorem is referenced by:  uneq2  3497  uneq12  3498  uneq1i  3499  uneq1d  3502  unineq  3593  prprc1  3916  uniprg  4032  unexb  4712  relresfld  5399  relcoi1  5401  oarec  6808  xpider  6978  undifixp  7101  unxpdom  7319  enp1ilem  7345  findcard2  7351  domunfican  7382  pwfilem  7404  fin1a2lem10  8294  incexclem  12621  ramub1lem1  13399  ramub1  13401  mreexexlem3d  13876  mreexexlem4d  13877  ipodrsima  14596  mplsubglem  16503  mretopd  17161  iscldtop  17164  nconsubb  17491  plyval  20117  spanun  23052  difeq  24003  measun  24570  nofulllem2  25663  brsuccf  25791  altopthsn  25811  rankung  26112  ralxpmap  26756  nacsfix  26780  eldioph4b  26886  eldioph4i  26887  diophren  26888  compne  27633  islshp  29851  lshpset2N  29991  paddval  30669
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-un 3327
  Copyright terms: Public domain W3C validator