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

Theorem uneq1 4152
Description: Equality theorem for the union of two classes. (Contributed by NM, 15-Jul-1993.)
Assertion
Ref Expression
uneq1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))

Proof of Theorem uneq1
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eleq2 2821 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21orbi1d 915 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑥𝐶) ↔ (𝑥𝐵𝑥𝐶)))
3 elun 4144 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elun 4144 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
52, 3, 43bitr4g 313 . 2 (𝐴 = 𝐵 → (𝑥 ∈ (𝐴𝐶) ↔ 𝑥 ∈ (𝐵𝐶)))
65eqrdv 2729 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 845   = wceq 1541  wcel 2106  cun 3942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-un 3949
This theorem is referenced by:  uneq2  4153  uneq12  4154  uneq1i  4155  uneq1d  4158  unineq  4273  prprc1  4762  uniprgOLD  4921  relresfld  6264  unexb  7718  oarec  8545  xpider  8765  ralxpmap  8873  undifixp  8911  findcard2  9147  pwfilem  9160  unxpdom  9236  enp1ilem  9261  findcard2OLD  9267  domunfican  9303  pwfilemOLD  9329  fin1a2lem10  10386  incexclem  15764  lcmfunsnlem  16560  ramub1lem1  16941  ramub1  16943  mreexexlem3d  17572  mreexexlem4d  17573  ipodrsima  18476  mplsubglem  21487  mretopd  22525  iscldtop  22528  nconnsubb  22856  plyval  25636  spanun  30661  difeq  31620  unelldsys  32987  isros  32997  unelros  33000  difelros  33001  rossros  33009  measun  33040  inelcarsg  33141  actfunsnf1o  33447  actfunsnrndisj  33448  mrsubvrs  34344  altopthsn  34763  rankung  34968  bj-adjg1  35728  poimirlem28  36320  islshp  37654  lshpset2N  37794  paddval  38474  nacsfix  41221  eldioph4b  41320  eldioph4i  41321  diophren  41322  clsk3nimkb  42562  isotone1  42570  fiiuncl  43523  founiiun0  43659  infxrpnf  43929  meadjun  44951  hoidmvle  45089
  Copyright terms: Public domain W3C validator