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

Theorem uneq12i 3726
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 3723 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3mp2an 703 1 (𝐴𝐶) = (𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  cun 3537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544
This theorem is referenced by:  indir  3833  difundir  3838  difindi  3839  dfsymdif3  3851  unrab  3856  rabun2  3864  elnelun  3917  dfif6  4038  dfif3  4049  dfif5  4051  symdif0  4527  symdifid  4529  unopab  4654  xpundi  5084  xpundir  5085  xpun  5089  dmun  5240  resundi  5317  resundir  5318  cnvun  5443  rnun  5446  imaundi  5450  imaundir  5451  dmtpop  5515  coundi  5539  coundir  5540  unidmrn  5568  dfdm2  5570  predun  5607  mptun  5924  resasplit  5972  fresaun  5973  fresaunres2  5974  residpr  6300  fpr  6304  fvsnun2  6332  sbthlem5  7936  1sdom  8025  cdaassen  8864  fz0to3un2pr  12265  fz0to4untppr  12266  fzo0to42pr  12377  hashgval  12937  hashinf  12939  relexpcnv  13569  bpoly3  14574  vdwlem6  15474  setsres  15675  xpsc  15986  lefld  16995  opsrtoslem1  19251  volun  23037  iblcnlem1  23277  ex-dif  26438  ex-in  26440  ex-pw  26444  ex-xp  26451  ex-cnv  26452  ex-rn  26455  partfun  28664  ordtprsuni  29099  indval2  29210  sigaclfu2  29317  eulerpartgbij  29567  subfacp1lem1  30221  subfacp1lem5  30226  fixun  30992  refssfne  31329  onint1  31424  bj-pr1un  31987  bj-pr21val  31997  bj-pr2un  32001  bj-pr22val  32003  poimirlem16  32398  poimirlem19  32401  itg2addnclem2  32435  iblabsnclem  32446  rclexi  36744  rtrclex  36746  cnvrcl0  36754  dfrtrcl5  36758  dfrcl2  36788  dfrcl4  36790  iunrelexp0  36816  relexpiidm  36818  corclrcl  36821  relexp01min  36827  corcltrcl  36853  cotrclrcl  36856  frege131d  36878  df3o3  37146  31prm  39855  rnfdmpr  40141
  Copyright terms: Public domain W3C validator