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

Theorem uneq1 3718
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 2673 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21orbi1d 734 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑥𝐶) ↔ (𝑥𝐵𝑥𝐶)))
3 elun 3711 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elun 3711 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
52, 3, 43bitr4g 301 . 2 (𝐴 = 𝐵 → (𝑥 ∈ (𝐴𝐶) ↔ 𝑥 ∈ (𝐵𝐶)))
65eqrdv 2604 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 381   = wceq 1474  wcel 1976  cun 3534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-v 3171  df-un 3541
This theorem is referenced by:  uneq2  3719  uneq12  3720  uneq1i  3721  uneq1d  3724  unineq  3832  prprc1  4239  uniprg  4377  relresfld  5562  unexb  6830  oarec  7503  xpider  7679  ralxpmap  7767  undifixp  7804  unxpdom  8026  enp1ilem  8053  findcard2  8059  domunfican  8092  pwfilem  8117  fin1a2lem10  9088  incexclem  14350  lcmfunsnlem  15135  ramub1lem1  15511  ramub1  15513  mreexexlem3d  16072  mreexexlem4d  16073  ipodrsima  16931  mplsubglem  19198  mretopd  20645  iscldtop  20648  nconsubb  20975  plyval  23667  spanun  27591  difeq  28542  unelldsys  29351  isros  29361  unelros  29364  difelros  29365  rossros  29373  measun  29404  inelcarsg  29503  mrsubvrs  30476  nofulllem2  30905  altopthsn  31041  rankung  31246  poimirlem28  32407  islshp  33084  lshpset2N  33224  paddval  33902  nacsfix  36093  eldioph4b  36193  eldioph4i  36194  diophren  36195  clsk3nimkb  37158  isotone1  37166  compne  37465  fiiuncl  38059  founiiun0  38172  meadjun  39156  hoidmvle  39291
  Copyright terms: Public domain W3C validator