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

Theorem uneq1 4056
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 2822 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21orbi1d 916 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑥𝐶) ↔ (𝑥𝐵𝑥𝐶)))
3 elun 4049 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elun 4049 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
52, 3, 43bitr4g 317 . 2 (𝐴 = 𝐵 → (𝑥 ∈ (𝐴𝐶) ↔ 𝑥 ∈ (𝐵𝐶)))
65eqrdv 2737 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 846   = wceq 1542  wcel 2114  cun 3851
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3402  df-un 3858
This theorem is referenced by:  uneq2  4057  uneq12  4058  uneq1i  4059  uneq1d  4062  unineq  4178  prprc1  4666  uniprgOLD  4826  relresfld  6118  unexb  7502  oarec  8232  xpider  8412  ralxpmap  8519  undifixp  8557  findcard2  8776  pwfilem  8788  unxpdom  8817  enp1ilem  8842  findcard2OLD  8847  domunfican  8878  pwfilemOLD  8904  fin1a2lem10  9922  incexclem  15297  lcmfunsnlem  16095  ramub1lem1  16475  ramub1  16477  mreexexlem3d  17033  mreexexlem4d  17034  ipodrsima  17904  mplsubglem  20828  mretopd  21856  iscldtop  21859  nconnsubb  22187  plyval  24955  spanun  29493  difeq  30452  unelldsys  31709  isros  31719  unelros  31722  difelros  31723  rossros  31731  measun  31762  inelcarsg  31861  actfunsnf1o  32167  actfunsnrndisj  32168  mrsubvrs  33068  altopthsn  33919  rankung  34124  poimirlem28  35461  islshp  36649  lshpset2N  36789  paddval  37468  nacsfix  40147  eldioph4b  40246  eldioph4i  40247  diophren  40248  clsk3nimkb  41237  isotone1  41245  fiiuncl  42192  founiiun0  42307  infxrpnf  42566  meadjun  43583  hoidmvle  43721
  Copyright terms: Public domain W3C validator