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

Theorem uneq1 3744
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 2687 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21orbi1d 738 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑥𝐶) ↔ (𝑥𝐵𝑥𝐶)))
3 elun 3737 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elun 3737 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
52, 3, 43bitr4g 303 . 2 (𝐴 = 𝐵 → (𝑥 ∈ (𝐴𝐶) ↔ 𝑥 ∈ (𝐵𝐶)))
65eqrdv 2619 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 383   = wceq 1480  wcel 1987  cun 3558
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-un 3565
This theorem is referenced by:  uneq2  3745  uneq12  3746  uneq1i  3747  uneq1d  3750  unineq  3859  prprc1  4277  uniprg  4423  relresfld  5631  unexb  6923  oarec  7602  xpider  7778  ralxpmap  7867  undifixp  7904  unxpdom  8127  enp1ilem  8154  findcard2  8160  domunfican  8193  pwfilem  8220  fin1a2lem10  9191  incexclem  14512  lcmfunsnlem  15297  ramub1lem1  15673  ramub1  15675  mreexexlem3d  16246  mreexexlem4d  16247  ipodrsima  17105  mplsubglem  19374  mretopd  20836  iscldtop  20839  nconnsubb  21166  plyval  23887  spanun  28292  difeq  29243  unelldsys  30044  isros  30054  unelros  30057  difelros  30058  rossros  30066  measun  30097  inelcarsg  30196  mrsubvrs  31180  altopthsn  31763  rankung  31968  poimirlem28  33108  islshp  33785  lshpset2N  33925  paddval  34603  nacsfix  36794  eldioph4b  36894  eldioph4i  36895  diophren  36896  clsk3nimkb  37859  isotone1  37867  compneOLD  38165  fiiuncl  38756  founiiun0  38886  meadjun  40016  hoidmvle  40151
  Copyright terms: Public domain W3C validator