Theorem elex2 2820

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 2818	. 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 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 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 2213

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

This theorem is referenced by:  snmg  3794  oprcl  3891  brm  4144  ss1o0el1  4293  exss  4325  onintrab2im  4622  regexmidlemm  4636  reldmm  4956  dmxpid  4959  acexmidlem2  6025  elmpom  6412  frecabcl  6608  ixpm  6942  en1m  7022  dom1o  7045  dom1oi  7046  enm  7047  ssfilem  7105  ssfilemd  7107  fin0  7117  fin0or  7118  diffitest  7119  diffisn  7125  infm  7139  inffiexmid  7141  ctssdc  7372  omct  7376  ctssexmid  7409  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  acnrcl  7476  exmidaclem  7483  iftrueb01  7501  pw1if  7503  caucvgsrlemasr  8070  suplocsrlempr  8087  gtso  8317  sup3exmid  9196  indstr  9888  negm  9910  fzm  10335  fzom  10462  rexfiuz  11629  r19.2uz  11633  resqrexlemgt0  11660  climuni  11933  bezoutlembi  12656  nninfct  12692  lcmgcdlem  12729  pcprecl  12942  pc2dvds  12983  4sqlem13m  13056  nninfdclemcl  13149  dfgrp3m  13762  issubg2m  13856  issubgrpd2  13857  issubg3  13859  issubg4m  13860  grpissubg  13861  subgintm  13865  nmzsubg  13877  ghmrn  13924  ghmpreima  13933  dvdsr02  14200  01eq0ring  14284  subrgugrp  14335  lmodfopnelem1  14420  rmodislmodlem  14446  rmodislmod  14447  lss1  14458  lsssubg  14473  islss3  14475  islss4  14478  lss1d  14479  lssintclm  14480  dflidl2rng  14577  lidlsubg  14582  cnsubglem  14675  tgioo  15365  elply2  15546  edgval  16001  wlkvtxm  16281  pw1nct  16725  nninfall  16735  nnnninfen  16747