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 )

This proof depends on syntax axioms:   -> wi 4   A.wal 1400   = wceq 1402   E.wex 1545   e. wcel 2209

This proof depends on 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 proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is used by:  snmg  3831  oprcl  3928  brm  4181  ss1o0el1  4334  exss  4367  onintrab2im  4665  regexmidlemm  4679  reldmm  5000  dmxpid  5003  mptmex  5945  acexmidlem2  6082  elmpom  6474  frecabcl  6670  ixpm  7012  en1m  7092  dom1o  7116  dom1oi  7117  enm  7118  ssfilem  7177  ssfilemd  7179  fin0  7189  fin0or  7190  diffitest  7191  diffisn  7197  infm  7211  inffiexmid  7213  ctssdc  7453  omct  7457  ctssexmid  7490  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  acnrcl  7557  exmidaclem  7564  iftrueb01  7582  pw1if  7584  caucvgsrlemasr  8157  suplocsrlempr  8174  gtso  8404  sup3exmid  9289  indstr  10002  negm  10024  fzm  10452  fzom  10582  rexfiuz  11769  r19.2uz  11773  resqrexlemgt0  11800  climuni  12075  bezoutlembi  12798  nninfct  12834  lcmgcdlem  12871  pcprecl  13088  pc2dvds  13129  4sqlem13m  13202  nninfdclemcl  13388  dfgrp3m  13953  issubg2m  14041  issubgrpd2  14042  issubg3  14044  issubg4m  14045  grpissubg  14046  subgintm  14050  nmzsubg  14062  ghmrn  14109  ghmpreima  14118  dvdsr02  14461  01eq0ring  14545  subrgugrp  14597  lmodfopnelem1  14710  rmodislmodlem  14736  rmodislmod  14737  lss1  14748  lsssubg  14763  islss3  14765  islss4  14768  lss1d  14769  lssintclm  14770  dflidl2rng  14867  lidlsubg  14872  cnsubglem  14965  asplss  15065  aspsubrg  15067  tgioo  15704  elply2  15885  edgval  16399  wlkvtxm  16679  pw1nct  17131  rabid1o  17132  stnot  17137  nninfall  17150  nnnninfen  17162