Theorem elunii 4254

Description: Membership in class union. (Contributed by NM, 24-Mar-1995.)

Assertion

Ref	Expression
elunii

Proof of Theorem elunii

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2530	. . . . 5
2		eleq1 2529	. . . . 5
3	1, 2	anbi12d 710	. . . 4
4	3	spcegv 3195	. . 3
5	4	anabsi7 819	. 2
6		eluni 4252	. 2
7	5, 6	sylibr 212	1

Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  E.wex 1612  e.wcel 1818  U.cuni 4249

This theorem is referenced by:  ssuni  4271  unipw  4702  opeluu  4721  unon  6666  limuni3  6687  uniinqs  7410  trcl  8180  rankwflemb  8232  ac5num  8438  dfac3  8523  isf34lem4  8778  axcclem  8858  ttukeylem7  8916  brdom7disj  8930  brdom6disj  8931  wrdexb  12558  dprdfeq0  17062  dprdfeq0OLD  17069  tgss2  19489  ppttop  19508  isclo  19588  neips  19614  bwthOLD  19911  2ndcomap  19959  2ndcsep  19960  locfincmp  20027  comppfsc  20033  txkgen  20153  txcon  20190  basqtop  20212  nrmr0reg  20250  alexsublem  20544  alexsubALTlem4  20550  alexsubALT  20551  ptcmplem4  20555  unirnblps  20922  unirnbl  20923  blbas  20933  met2ndci  21025  bndth  21458  dyadmbllem  22008  opnmbllem  22010  dya2iocnei  28253  dstfrvunirn  28413  pconcon  28676  cvmcov2  28720  cvmlift2lem11  28758  cvmlift2lem12  28759  onint1  29914  opnmbllem0  30050  neibastop2lem  30178  heibor1  30306  unichnidl  30428  prtlem16  30610  prter2  30622  stoweidlem43  31825  stoweidlem55  31837  truniALT  33312  unipwrVD  33632  unipwr  33633  truniALTVD  33678  unisnALT  33726

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-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-uni 4250