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

Theorem uneq1 4136
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 2906 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21orbi1d 912 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑥𝐶) ↔ (𝑥𝐵𝑥𝐶)))
3 elun 4129 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elun 4129 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
52, 3, 43bitr4g 315 . 2 (𝐴 = 𝐵 → (𝑥 ∈ (𝐴𝐶) ↔ 𝑥 ∈ (𝐵𝐶)))
65eqrdv 2824 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 843   = wceq 1530  wcel 2107  cun 3938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-un 3945
This theorem is referenced by:  uneq2  4137  uneq12  4138  uneq1i  4139  uneq1d  4142  unineq  4258  prprc1  4700  uniprg  4851  relresfld  6125  unexb  7460  oarec  8178  xpider  8358  ralxpmap  8449  undifixp  8487  unxpdom  8714  enp1ilem  8741  findcard2  8747  domunfican  8780  pwfilem  8807  fin1a2lem10  9820  incexclem  15181  lcmfunsnlem  15975  ramub1lem1  16352  ramub1  16354  mreexexlem3d  16907  mreexexlem4d  16908  ipodrsima  17765  mplsubglem  20133  mretopd  21619  iscldtop  21622  nconnsubb  21950  plyval  24701  spanun  29239  difeq  30197  unelldsys  31306  isros  31316  unelros  31319  difelros  31320  rossros  31328  measun  31359  inelcarsg  31458  actfunsnf1o  31764  actfunsnrndisj  31765  mrsubvrs  32656  altopthsn  33309  rankung  33514  poimirlem28  34790  islshp  35985  lshpset2N  36125  paddval  36804  nacsfix  39177  eldioph4b  39276  eldioph4i  39277  diophren  39278  clsk3nimkb  40258  isotone1  40266  fiiuncl  41195  founiiun0  41319  infxrpnf  41589  meadjun  42613  hoidmvle  42751
  Copyright terms: Public domain W3C validator