Theorem elex2 2819

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 2817	. 2 |- ( A e. B -> E. x x = A )
4		exim 1647	. 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 1395   = wceq 1397   E.wex 1540   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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  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 2804

This theorem is referenced by:  snmg  3790  oprcl  3886  brm  4139  ss1o0el1  4287  exss  4319  onintrab2im  4616  regexmidlemm  4630  reldmm  4950  dmxpid  4953  acexmidlem2  6015  elmpom  6403  frecabcl  6565  ixpm  6899  en1m  6979  dom1o  7002  dom1oi  7003  enm  7004  ssfilem  7062  ssfilemd  7064  fin0  7074  fin0or  7075  diffitest  7076  diffisn  7082  infm  7096  inffiexmid  7098  ctssdc  7312  omct  7316  ctssexmid  7349  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  acnrcl  7416  exmidaclem  7423  iftrueb01  7441  pw1if  7443  caucvgsrlemasr  8010  suplocsrlempr  8027  gtso  8258  sup3exmid  9137  indstr  9827  negm  9849  fzm  10273  fzom  10400  rexfiuz  11567  r19.2uz  11571  resqrexlemgt0  11598  climuni  11871  bezoutlembi  12594  nninfct  12630  lcmgcdlem  12667  pcprecl  12880  pc2dvds  12921  4sqlem13m  12994  nninfdclemcl  13087  dfgrp3m  13700  issubg2m  13794  issubgrpd2  13795  issubg3  13797  issubg4m  13798  grpissubg  13799  subgintm  13803  nmzsubg  13815  ghmrn  13862  ghmpreima  13871  dvdsr02  14138  01eq0ring  14222  subrgugrp  14273  lmodfopnelem1  14357  rmodislmodlem  14383  rmodislmod  14384  lss1  14395  lsssubg  14410  islss3  14412  islss4  14415  lss1d  14416  lssintclm  14417  dflidl2rng  14514  lidlsubg  14519  cnsubglem  14612  tgioo  15297  elply2  15478  edgval  15930  wlkvtxm  16210  pw1nct  16655  nninfall  16662  nnnninfen  16674