Theorem elex2 2832

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 2306	. . 3 |- ( A e. B -> ( x = A -> x e. B ) )
2	1	alrimiv 1923	. 2 |- ( A e. B -> A. x ( x = A -> x e. B ) )
3		elisset 2830	. 2 |- ( A e. B -> E. x x = A )
4		exim 1648	. 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 1396   = wceq 1398   E.wex 1541   e. wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-v 2817

This theorem is referenced by:  snmg  3815  oprcl  3912  brm  4165  ss1o0el1  4315  exss  4348  onintrab2im  4645  regexmidlemm  4659  reldmm  4980  dmxpid  4983  acexmidlem2  6055  elmpom  6447  frecabcl  6643  ixpm  6978  en1m  7058  dom1o  7082  dom1oi  7083  enm  7084  ssfilem  7143  ssfilemd  7145  fin0  7155  fin0or  7156  diffitest  7157  diffisn  7163  infm  7177  inffiexmid  7179  ctssdc  7417  omct  7421  ctssexmid  7454  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  acnrcl  7521  exmidaclem  7528  iftrueb01  7546  pw1if  7548  caucvgsrlemasr  8121  suplocsrlempr  8138  gtso  8368  sup3exmid  9248  indstr  9943  negm  9965  fzm  10392  fzom  10521  rexfiuz  11699  r19.2uz  11703  resqrexlemgt0  11730  climuni  12003  bezoutlembi  12726  nninfct  12762  lcmgcdlem  12799  pcprecl  13012  pc2dvds  13053  4sqlem13m  13126  nninfdclemcl  13283  dfgrp3m  13854  issubg2m  13942  issubgrpd2  13943  issubg3  13945  issubg4m  13946  grpissubg  13947  subgintm  13951  nmzsubg  13963  ghmrn  14010  ghmpreima  14019  dvdsr02  14350  01eq0ring  14434  subrgugrp  14486  lmodfopnelem1  14598  rmodislmodlem  14624  rmodislmod  14625  lss1  14636  lsssubg  14651  islss3  14653  islss4  14656  lss1d  14657  lssintclm  14658  dflidl2rng  14755  lidlsubg  14760  cnsubglem  14853  tgioo  15545  elply2  15726  edgval  16181  wlkvtxm  16461  pw1nct  16903  nninfall  16913  nnnninfen  16925