Theorem elex2 2793

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 2279	. . 3 |- ( A e. B -> ( x = A -> x e. B ) )
2	1	alrimiv 1898	. 2 |- ( A e. B -> A. x ( x = A -> x e. B ) )
3		elisset 2791	. 2 |- ( A e. B -> E. x x = A )
4		exim 1623	. 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 1516   e. wcel 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-v 2778

This theorem is referenced by:  snmg  3761  oprcl  3857  brm  4110  ss1o0el1  4257  exss  4289  onintrab2im  4584  regexmidlemm  4598  dmxpid  4918  acexmidlem2  5964  frecabcl  6508  ixpm  6840  en1m  6920  enm  6940  ssfilem  6998  fin0  7008  fin0or  7009  diffitest  7010  diffisn  7016  infm  7027  inffiexmid  7029  ctssdc  7241  omct  7245  ctssexmid  7278  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  acnrcl  7344  exmidaclem  7351  iftrueb01  7369  pw1if  7371  caucvgsrlemasr  7938  suplocsrlempr  7955  gtso  8186  sup3exmid  9065  indstr  9749  negm  9771  fzm  10195  fzom  10322  rexfiuz  11415  r19.2uz  11419  resqrexlemgt0  11446  climuni  11719  bezoutlembi  12441  nninfct  12477  lcmgcdlem  12514  pcprecl  12727  pc2dvds  12768  4sqlem13m  12841  nninfdclemcl  12934  dfgrp3m  13546  issubg2m  13640  issubgrpd2  13641  issubg3  13643  issubg4m  13644  grpissubg  13645  subgintm  13649  nmzsubg  13661  ghmrn  13708  ghmpreima  13717  dvdsr02  13982  01eq0ring  14066  subrgugrp  14117  lmodfopnelem1  14201  rmodislmodlem  14227  rmodislmod  14228  lss1  14239  lsssubg  14254  islss3  14256  islss4  14259  lss1d  14260  lssintclm  14261  dflidl2rng  14358  lidlsubg  14363  cnsubglem  14456  tgioo  15141  elply2  15322  dom1o  16128  pw1nct  16142  nninfall  16148  nnnninfen  16160