Theorem uneq1 3650

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

Assertion

Ref	Expression
uneq1

Proof of Theorem uneq1

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2530	. . . 4
2	1	orbi1d 702	. . 3
3		elun 3644	. . 3
4		elun 3644	. . 3
5	2, 3, 4	3bitr4g 288	. 2
6	5	eqrdv 2454	1

Syntax hints:  ->wi 4  \/wo 368  =wceq 1395  e.wcel 1818  u.cun 3473

This theorem is referenced by:  uneq2  3651  uneq12  3652  uneq1i  3653  uneq1d  3656  unineq  3747  prprc1  4140  uniprg  4263  relresfld  5539  relcoi1  5541  unexb  6600  oarec  7230  xpider  7401  ralxpmap  7488  undifixp  7525  unxpdom  7747  enp1ilem  7774  findcard2  7780  domunfican  7813  pwfilem  7834  fin1a2lem10  8810  incexclem  13648  ramub1lem1  14544  ramub1  14546  mreexexlem3d  15043  mreexexlem4d  15044  ipodrsima  15795  mplsubglem  18093  mplsubglemOLD  18095  mretopd  19593  iscldtop  19596  nconsubb  19924  plyval  22590  spanun  26463  difeq  27416  measun  28182  mrsubvrs  28882  nofulllem2  29463  brsuccf  29591  altopthsn  29611  rankung  29823  nacsfix  30644  eldioph4b  30745  eldioph4i  30746  diophren  30747  compne  31349  islshp  34704  lshpset2N  34844  paddval  35522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480