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  9287  indstr  9993  negm  10015  fzm  10442  fzom  10572  rexfiuz  11755  r19.2uz  11759  resqrexlemgt0  11786  climuni  12059  bezoutlembi  12782  nninfct  12818  lcmgcdlem  12855  pcprecl  13068  pc2dvds  13109  4sqlem13m  13182  nninfdclemcl  13339  dfgrp3m  13904  issubg2m  13992  issubgrpd2  13993  issubg3  13995  issubg4m  13996  grpissubg  13997  subgintm  14001  nmzsubg  14013  ghmrn  14060  ghmpreima  14069  dvdsr02  14412  01eq0ring  14496  subrgugrp  14548  lmodfopnelem1  14661  rmodislmodlem  14687  rmodislmod  14688  lss1  14699  lsssubg  14714  islss3  14716  islss4  14719  lss1d  14720  lssintclm  14721  dflidl2rng  14818  lidlsubg  14823  cnsubglem  14916  asplss  15016  aspsubrg  15018  tgioo  15655  elply2  15836  edgval  16301  wlkvtxm  16581  pw1nct  17033  rabid1o  17034  stnot  17039  nninfall  17052  nnnninfen  17064