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

Theorem uneq1 3793
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 2719 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21orbi1d 739 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑥𝐶) ↔ (𝑥𝐵𝑥𝐶)))
3 elun 3786 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elun 3786 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
52, 3, 43bitr4g 303 . 2 (𝐴 = 𝐵 → (𝑥 ∈ (𝐴𝐶) ↔ 𝑥 ∈ (𝐵𝐶)))
65eqrdv 2649 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382   = wceq 1523  wcel 2030  cun 3605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612
This theorem is referenced by:  uneq2  3794  uneq12  3795  uneq1i  3796  uneq1d  3799  unineq  3910  prprc1  4332  uniprg  4482  relresfld  5700  unexb  7000  oarec  7687  xpider  7861  ralxpmap  7949  undifixp  7986  unxpdom  8208  enp1ilem  8235  findcard2  8241  domunfican  8274  pwfilem  8301  fin1a2lem10  9269  incexclem  14612  lcmfunsnlem  15401  ramub1lem1  15777  ramub1  15779  mreexexlem3d  16353  mreexexlem4d  16354  ipodrsima  17212  mplsubglem  19482  mretopd  20944  iscldtop  20947  nconnsubb  21274  plyval  23994  spanun  28532  difeq  29481  unelldsys  30349  isros  30359  unelros  30362  difelros  30363  rossros  30371  measun  30402  inelcarsg  30501  actfunsnf1o  30810  actfunsnrndisj  30811  mrsubvrs  31545  altopthsn  32193  rankung  32398  poimirlem28  33567  islshp  34584  lshpset2N  34724  paddval  35402  nacsfix  37592  eldioph4b  37692  eldioph4i  37693  diophren  37694  clsk3nimkb  38655  isotone1  38663  compneOLD  38961  fiiuncl  39548  founiiun0  39691  infxrpnf  39987  meadjun  40997  hoidmvle  41135
  Copyright terms: Public domain W3C validator