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

Theorem uneq1 4129
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 2898 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
21orbi1d 910 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑥𝐶) ↔ (𝑥𝐵𝑥𝐶)))
3 elun 4122 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
4 elun 4122 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
52, 3, 43bitr4g 315 . 2 (𝐴 = 𝐵 → (𝑥 ∈ (𝐴𝐶) ↔ 𝑥 ∈ (𝐵𝐶)))
65eqrdv 2816 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 841   = wceq 1528  wcel 2105  cun 3931
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938
This theorem is referenced by:  uneq2  4130  uneq12  4131  uneq1i  4132  uneq1d  4135  unineq  4251  prprc1  4693  uniprg  4844  relresfld  6120  unexb  7460  oarec  8177  xpider  8357  ralxpmap  8448  undifixp  8486  unxpdom  8713  enp1ilem  8740  findcard2  8746  domunfican  8779  pwfilem  8806  fin1a2lem10  9819  incexclem  15179  lcmfunsnlem  15973  ramub1lem1  16350  ramub1  16352  mreexexlem3d  16905  mreexexlem4d  16906  ipodrsima  17763  mplsubglem  20142  mretopd  21628  iscldtop  21631  nconnsubb  21959  plyval  24710  spanun  29249  difeq  30207  unelldsys  31316  isros  31326  unelros  31329  difelros  31330  rossros  31338  measun  31369  inelcarsg  31468  actfunsnf1o  31774  actfunsnrndisj  31775  mrsubvrs  32666  altopthsn  33319  rankung  33524  poimirlem28  34801  islshp  35995  lshpset2N  36135  paddval  36814  nacsfix  39187  eldioph4b  39286  eldioph4i  39287  diophren  39288  clsk3nimkb  40268  isotone1  40276  fiiuncl  41204  founiiun0  41327  infxrpnf  41597  meadjun  42621  hoidmvle  42759
  Copyright terms: Public domain W3C validator