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

Theorem uneq12i 4123
 Description: Equality inference for the union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
Hypotheses
Ref Expression
uneq1i.1 𝐴 = 𝐵
uneq12i.2 𝐶 = 𝐷
Assertion
Ref Expression
uneq12i (𝐴𝐶) = (𝐵𝐷)

Proof of Theorem uneq12i
StepHypRef Expression
1 uneq1i.1 . 2 𝐴 = 𝐵
2 uneq12i.2 . 2 𝐶 = 𝐷
3 uneq12 4120 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3mp2an 691 1 (𝐴𝐶) = (𝐵𝐷)
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538   ∪ cun 3917 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924 This theorem is referenced by:  indir  4237  difundir  4242  difindi  4243  dfsymdif3  4254  unrab  4259  rabun2  4267  elnelun  4326  dfif6  4453  dfif3  4464  dfif5  4466  symdif0  4994  symdifid  4996  unopab  5132  xpundi  5608  xpundir  5609  xpun  5613  dmun  5767  resundi  5855  resundir  5856  cnvun  5989  rnun  5992  imaundi  5996  imaundir  5997  dmtpop  6063  coundi  6088  coundir  6089  unidmrn  6118  dfdm2  6120  predun  6160  mptun  6483  resasplit  6537  fresaun  6538  fresaunres2  6539  residpr  6894  fpr  6905  sbthlem5  8624  1sdom  8714  djuassen  9598  fz0to3un2pr  13011  fz0to4untppr  13012  fzo0to42pr  13126  hashgval  13696  hashinf  13698  relexpcnv  14392  bpoly3  15410  vdwlem6  16318  setsres  16523  lefld  17834  opsrtoslem1  20259  volun  24147  ex-dif  28206  ex-in  28208  ex-pw  28212  ex-xp  28219  ex-cnv  28220  ex-rn  28223  partfun  30427  fzodif1  30522  ordtprsuni  31189  indval2  31300  sigaclfu2  31407  eulerpartgbij  31657  subfacp1lem1  32453  subfacp1lem5  32458  fmla1  32661  fixun  33397  refssfne  33733  onint1  33824  bj-pr1un  34353  bj-pr21val  34363  bj-pr2un  34367  bj-pr22val  34369  poimirlem16  34985  poimirlem19  34988  itg2addnclem2  35021  iblabsnclem  35032  rclexi  40171  rtrclex  40173  cnvrcl0  40181  dfrtrcl5  40185  dfrcl2  40231  dfrcl4  40233  iunrelexp0  40259  relexpiidm  40261  corclrcl  40264  relexp01min  40270  corcltrcl  40296  cotrclrcl  40299  frege131d  40321  df3o3  40587  rnfdmpr  43703  31prm  43980
 Copyright terms: Public domain W3C validator