Theorem elex2 2838

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 2310	. . 3 |- ( A e. B -> ( x = A -> x e. B ) )
2	1	alrimiv 1927	. 2 |- ( A e. B -> A. x ( x = A -> x e. B ) )
3		elisset 2836	. 2 |- ( A e. B -> E. x x = A )
4		exim 1652	. 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 1400   = wceq 1402   E.wex 1545   e. wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is referenced by:  snmg  3826  oprcl  3923  brm  4176  ss1o0el1  4329  exss  4362  onintrab2im  4660  regexmidlemm  4674  reldmm  4995  dmxpid  4998  acexmidlem2  6072  elmpom  6464  frecabcl  6660  ixpm  7002  en1m  7082  dom1o  7106  dom1oi  7107  enm  7108  ssfilem  7167  ssfilemd  7169  fin0  7179  fin0or  7180  diffitest  7181  diffisn  7187  infm  7201  inffiexmid  7203  ctssdc  7443  omct  7447  ctssexmid  7480  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  acnrcl  7547  exmidaclem  7554  iftrueb01  7572  pw1if  7574  caucvgsrlemasr  8147  suplocsrlempr  8164  gtso  8394  sup3exmid  9277  indstr  9972  negm  9994  fzm  10421  fzom  10550  rexfiuz  11733  r19.2uz  11737  resqrexlemgt0  11764  climuni  12037  bezoutlembi  12760  nninfct  12796  lcmgcdlem  12833  pcprecl  13046  pc2dvds  13087  4sqlem13m  13160  nninfdclemcl  13317  dfgrp3m  13881  issubg2m  13969  issubgrpd2  13970  issubg3  13972  issubg4m  13973  grpissubg  13974  subgintm  13978  nmzsubg  13990  ghmrn  14037  ghmpreima  14046  dvdsr02  14385  01eq0ring  14469  subrgugrp  14521  lmodfopnelem1  14633  rmodislmodlem  14659  rmodislmod  14660  lss1  14671  lsssubg  14686  islss3  14688  islss4  14691  lss1d  14692  lssintclm  14693  dflidl2rng  14790  lidlsubg  14795  cnsubglem  14888  tgioo  15578  elply2  15759  edgval  16215  wlkvtxm  16495  pw1nct  16947  nninfall  16957  nnnninfen  16969