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

Theorem uneq1 4160
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 2829 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21orbi1d 916 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑥𝐶) ↔ (𝑥𝐵𝑥𝐶)))
3 elun 4152 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elun 4152 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
52, 3, 43bitr4g 314 . 2 (𝐴 = 𝐵 → (𝑥 ∈ (𝐴𝐶) ↔ 𝑥 ∈ (𝐵𝐶)))
65eqrdv 2734 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 847   = wceq 1539  wcel 2107  cun 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3955
This theorem is referenced by:  uneq2  4161  uneq12  4162  uneq1i  4163  uneq1d  4166  unineq  4287  prprc1  4764  relresfld  6295  unexbOLD  7769  oarec  8601  xpider  8829  ralxpmap  8937  undifixp  8975  findcard2  9205  unxpdom  9290  enp1ilem  9313  pwfilem  9357  domunfican  9362  fin1a2lem10  10450  incexclem  15873  lcmfunsnlem  16679  ramub1lem1  17065  ramub1  17067  mreexexlem3d  17690  mreexexlem4d  17691  ipodrsima  18587  mplsubglem  22020  mretopd  23101  iscldtop  23104  nconnsubb  23432  plyval  26233  spanun  31565  difeq  32538  unelldsys  34160  isros  34170  unelros  34173  difelros  34174  rossros  34182  measun  34213  inelcarsg  34314  actfunsnf1o  34620  actfunsnrndisj  34621  mrsubvrs  35528  altopthsn  35963  rankung  36168  bj-adjg1  37045  poimirlem28  37656  islshp  38981  lshpset2N  39121  paddval  39801  nacsfix  42728  eldioph4b  42827  eldioph4i  42828  diophren  42829  clsk3nimkb  44058  isotone1  44066  fiiuncl  45075  founiiun0  45200  infxrpnf  45462  meadjun  46482  hoidmvle  46620
  Copyright terms: Public domain W3C validator