Theorem uneq12i 2234

Description: Equality inference for union of two classes. (The proof was shortened by Eric Schmidt, 26-Jan-2007.)

Hypotheses

Ref	Expression
uneq1i.1	|- A = B
uneq12i.2	|- C = D

Assertion

Ref	Expression
uneq12i	|- (A u. C) = (B u. D)

Proof of Theorem uneq12i

Step	Hyp	Ref	Expression
1		uneq1i.1	. 2 |- A = B
2		uneq12i.2	. 2 |- C = D
3		uneq12 2231	. 2 |- ((A = B /\ C = D) -> (A u. C) = (B u. D))
4	1, 2, 3	mp2an 701	1 |- (A u. C) = (B u. D)

Syntax hints:   = wceq 992   u. cun 2097

This theorem is referenced by:  indir 2305  difundir 2310  difindi 2311  symdif1 2317  unrab 2322  iunun 2683  unopab 2753  xpundi 3310  xpundir 3311  xpun 3312  resundi 3465  resundir 3466  rnun 3542  imaundi 3545  imaundir 3546  unidmrn 3621  fvsnun2 3908  df2o2 4277  sbthlem5 4596  rankpr 4838  rankelun 4853  cbvsumi 7189  acdc2lem2 7701  acdc5lem2 7704  ruclem6 7727  dispos 10881  refssfne 11565  isufil2 11650  ufileu 11658

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-un 2102

Copyright terms: Public domain