Theorem elex2 2819

Description: If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.)

Assertion

Ref	Expression
elex2	|- ( A e. B -> E. x x e. B )

Distinct variable groups:   x, A   x, B

Proof of Theorem elex2

Step	Hyp	Ref	Expression
1		eleq1a 2303	. . 3 |- ( A e. B -> ( x = A -> x e. B ) )
2	1	alrimiv 1922	. 2 |- ( A e. B -> A. x ( x = A -> x e. B ) )
3		elisset 2817	. 2 |- ( A e. B -> E. x x = A )
4		exim 1647	. 2 |- ( A. x ( x = A -> x e. B ) -> ( E. x x = A -> E. x x e. B ) )
5	2, 3, 4	sylc 62	1 |- ( A e. B -> E. x x e. B )

Syntax hints:   -> wi 4   A.wal 1395   = wceq 1397   E.wex 1540   e. wcel 2202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2804

This theorem is referenced by:  snmg  3790  oprcl  3886  brm  4139  ss1o0el1  4287  exss  4319  onintrab2im  4616  regexmidlemm  4630  reldmm  4950  dmxpid  4953  acexmidlem2  6015  elmpom  6403  frecabcl  6565  ixpm  6899  en1m  6979  dom1o  7002  dom1oi  7003  enm  7004  ssfilem  7062  ssfilemd  7064  fin0  7074  fin0or  7075  diffitest  7076  diffisn  7082  infm  7096  inffiexmid  7098  ctssdc  7312  omct  7316  ctssexmid  7349  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  acnrcl  7416  exmidaclem  7423  iftrueb01  7441  pw1if  7443  caucvgsrlemasr  8010  suplocsrlempr  8027  gtso  8258  sup3exmid  9137  indstr  9827  negm  9849  fzm  10273  fzom  10400  rexfiuz  11550  r19.2uz  11554  resqrexlemgt0  11581  climuni  11854  bezoutlembi  12577  nninfct  12613  lcmgcdlem  12650  pcprecl  12863  pc2dvds  12904  4sqlem13m  12977  nninfdclemcl  13070  dfgrp3m  13683  issubg2m  13777  issubgrpd2  13778  issubg3  13780  issubg4m  13781  grpissubg  13782  subgintm  13786  nmzsubg  13798  ghmrn  13845  ghmpreima  13854  dvdsr02  14121  01eq0ring  14205  subrgugrp  14256  lmodfopnelem1  14340  rmodislmodlem  14366  rmodislmod  14367  lss1  14378  lsssubg  14393  islss3  14395  islss4  14398  lss1d  14399  lssintclm  14400  dflidl2rng  14497  lidlsubg  14502  cnsubglem  14595  tgioo  15280  elply2  15461  edgval  15913  wlkvtxm  16193  pw1nct  16607  nninfall  16614  nnnninfen  16626