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

Theorem uneq12i 3631
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 3628 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3mp2an 703 1 (𝐴𝐶) = (𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  cun 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-v 3079  df-un 3449
This theorem is referenced by:  indir  3737  difundir  3742  difindi  3743  dfsymdif3  3755  unrab  3760  rabun2  3768  elnelun  3821  dfif6  3942  dfif3  3953  dfif5  3955  symdif0  4431  symdifid  4433  unopab  4558  xpundi  4988  xpundir  4989  xpun  4993  dmun  5144  resundi  5221  resundir  5222  cnvun  5347  rnun  5350  imaundi  5354  imaundir  5355  dmtpop  5419  coundi  5443  coundir  5444  unidmrn  5472  dfdm2  5474  predun  5511  mptun  5823  resasplit  5870  fresaun  5871  fresaunres2  5872  residpr  6198  fpr  6202  fvsnun2  6230  sbthlem5  7834  1sdom  7923  cdaassen  8762  fz0to3un2pr  12177  fz0to4untppr  12178  fzo0to42pr  12289  hashgval  12849  hashinf  12851  relexpcnv  13480  bpoly3  14495  vdwlem6  15410  setsres  15611  xpsc  15930  lefld  16939  opsrtoslem1  19207  volun  22996  iblcnlem1  23236  ex-dif  26411  ex-in  26413  ex-pw  26417  ex-xp  26424  ex-cnv  26425  ex-rn  26428  partfun  28647  ordtprsuni  29090  indval2  29201  sigaclfu2  29308  eulerpartgbij  29569  subfacp1lem1  30261  subfacp1lem5  30266  fixun  31022  refssfne  31358  onint1  31453  bj-pr1un  32016  bj-pr21val  32026  bj-pr2un  32030  bj-pr22val  32032  poimirlem16  32470  poimirlem19  32473  itg2addnclem2  32507  iblabsnclem  32518  rclexi  36823  rtrclex  36825  cnvrcl0  36833  dfrtrcl5  36837  dfrcl2  36867  dfrcl4  36869  iunrelexp0  36895  relexpiidm  36897  corclrcl  36900  relexp01min  36906  corcltrcl  36932  cotrclrcl  36935  frege131d  36957  df3o3  37225  31prm  39945  rnfdmpr  40231
  Copyright terms: Public domain W3C validator