Theorem elex2 2788

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 2277	. . 3 |- ( A e. B -> ( x = A -> x e. B ) )
2	1	alrimiv 1897	. 2 |- ( A e. B -> A. x ( x = A -> x e. B ) )
3		elisset 2786	. 2 |- ( A e. B -> E. x x = A )
4		exim 1622	. 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 1371   = wceq 1373   E.wex 1515   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-v 2774

This theorem is referenced by:  snmg  3751  oprcl  3843  brm  4094  ss1o0el1  4241  exss  4271  onintrab2im  4566  regexmidlemm  4580  dmxpid  4899  acexmidlem2  5941  frecabcl  6485  ixpm  6817  enm  6915  ssfilem  6972  fin0  6982  fin0or  6983  diffitest  6984  diffisn  6990  infm  7001  inffiexmid  7003  ctssdc  7215  omct  7219  ctssexmid  7252  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  acnrcl  7313  exmidaclem  7320  caucvgsrlemasr  7903  suplocsrlempr  7920  gtso  8151  sup3exmid  9030  indstr  9714  negm  9736  fzm  10160  fzom  10287  rexfiuz  11300  r19.2uz  11304  resqrexlemgt0  11331  climuni  11604  bezoutlembi  12326  nninfct  12362  lcmgcdlem  12399  pcprecl  12612  pc2dvds  12653  4sqlem13m  12726  nninfdclemcl  12819  dfgrp3m  13431  issubg2m  13525  issubgrpd2  13526  issubg3  13528  issubg4m  13529  grpissubg  13530  subgintm  13534  nmzsubg  13546  ghmrn  13593  ghmpreima  13602  dvdsr02  13867  01eq0ring  13951  subrgugrp  14002  lmodfopnelem1  14086  rmodislmodlem  14112  rmodislmod  14113  lss1  14124  lsssubg  14139  islss3  14141  islss4  14144  lss1d  14145  lssintclm  14146  dflidl2rng  14243  lidlsubg  14248  cnsubglem  14341  tgioo  15026  elply2  15207  pw1nct  15940  nninfall  15946  nnnninfen  15958