Theorem uneq1 3274

Description: Equality theorem for union of two classes. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Proof of Theorem uneq1

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2234	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
2	1	orbi1d 786	. . 3 |- ( A = B -> ( ( x e. A \/ x e. C ) <-> ( x e. B \/ x e. C ) ) )
3		elun 3268	. . 3 |- ( x e. ( A u. C ) <-> ( x e. A \/ x e. C ) )
4		elun 3268	. . 3 |- ( x e. ( B u. C ) <-> ( x e. B \/ x e. C ) )
5	2, 3, 4	3bitr4g 222	. 2 |- ( A = B -> ( x e. ( A u. C ) <-> x e. ( B u. C ) ) )
6	5	eqrdv 2168	1 |- ( A = B -> ( A u. C ) = ( B u. C ) )

Syntax hints:   -> wi 4   \/ wo 703   = wceq 1348   e. wcel 2141   u. cun 3119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125

This theorem is referenced by:  uneq2  3275  uneq12  3276  uneq1i  3277  uneq1d  3280  prprc1  3691  uniprg  3811  unexb  4427  relresfld  5140  relcoi1  5142  rdgeq2  6351  xpider  6584  findcard2  6867  findcard2s  6868  unfiexmid  6895  bdunexb  13955  bj-unexg  13956  exmid1stab  14033