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  4095  ss1o0el1  4242  exss  4272  onintrab2im  4567  regexmidlemm  4581  dmxpid  4900  acexmidlem2  5943  frecabcl  6487  ixpm  6819  enm  6917  ssfilem  6974  fin0  6984  fin0or  6985  diffitest  6986  diffisn  6992  infm  7003  inffiexmid  7005  ctssdc  7217  omct  7221  ctssexmid  7254  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  acnrcl  7315  exmidaclem  7322  caucvgsrlemasr  7905  suplocsrlempr  7922  gtso  8153  sup3exmid  9032  indstr  9716  negm  9738  fzm  10162  fzom  10289  rexfiuz  11333  r19.2uz  11337  resqrexlemgt0  11364  climuni  11637  bezoutlembi  12359  nninfct  12395  lcmgcdlem  12432  pcprecl  12645  pc2dvds  12686  4sqlem13m  12759  nninfdclemcl  12852  dfgrp3m  13464  issubg2m  13558  issubgrpd2  13559  issubg3  13561  issubg4m  13562  grpissubg  13563  subgintm  13567  nmzsubg  13579  ghmrn  13626  ghmpreima  13635  dvdsr02  13900  01eq0ring  13984  subrgugrp  14035  lmodfopnelem1  14119  rmodislmodlem  14145  rmodislmod  14146  lss1  14157  lsssubg  14172  islss3  14174  islss4  14177  lss1d  14178  lssintclm  14179  dflidl2rng  14276  lidlsubg  14281  cnsubglem  14374  tgioo  15059  elply2  15240  pw1nct  15977  nninfall  15983  nnnninfen  15995