Theorem uneq1 2180

Description: Equality theorem for union of two classes.

Assertion

Ref	Expression
uneq1	|- (A = B -> (A u. C) = (B u. C))

Proof of Theorem uneq1

Step	Hyp	Ref	Expression
1		eleq2 1538	. . . 4 |- (A = B -> (x e. A <-> x e. B))
2	1	orbi1d 617	. . 3 |- (A = B -> ((x e. A \/ x e. C) <-> (x e. B \/ x e. C)))
3		elun 2176	. . 3 |- (x e. (A u. C) <-> (x e. A \/ x e. C))
4		elun 2176	. . 3 |- (x e. (B u. C) <-> (x e. B \/ x e. C))
5	2, 3, 4	3bitr4g 557	. 2 |- (A = B -> (x e. (A u. C) <-> x e. (B u. C)))
6	5	eqrdv 1476	1 |- (A = B -> (A u. C) = (B u. C))

Syntax hints:   -> wi 3   \/ wo 222   = wceq 958   e. wcel 960   u. cun 2048

This theorem is referenced by:  uneq2 2181  uneq12 2182  uneq1i 2183  uneq1d 2186  unineq 2258  prprc1 2456  uniprg 2520  unexb 2879  suceq 3040  pwfilem 4577  pwfilemOLD 4578  unxpdom 4855  sshjvalt 9315  spanunt 9463

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-un 2053

Copyright terms: Public domain