Theorem elex2 2776

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 2265	. . 3 |- ( A e. B -> ( x = A -> x e. B ) )
2	1	alrimiv 1885	. 2 |- ( A e. B -> A. x ( x = A -> x e. B ) )
3		elisset 2774	. 2 |- ( A e. B -> E. x x = A )
4		exim 1610	. 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 1362   = wceq 1364   E.wex 1503   e. wcel 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-v 2762

This theorem is referenced by:  snmg  3737  oprcl  3829  brm  4080  ss1o0el1  4227  exss  4257  onintrab2im  4551  regexmidlemm  4565  dmxpid  4884  acexmidlem2  5916  frecabcl  6454  ixpm  6786  enm  6876  ssfilem  6933  fin0  6943  fin0or  6944  diffitest  6945  diffisn  6951  infm  6962  inffiexmid  6964  ctssdc  7174  omct  7178  ctssexmid  7211  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidaclem  7270  caucvgsrlemasr  7852  suplocsrlempr  7869  gtso  8100  sup3exmid  8978  indstr  9661  negm  9683  fzm  10107  fzom  10234  rexfiuz  11136  r19.2uz  11140  resqrexlemgt0  11167  climuni  11439  bezoutlembi  12145  nninfct  12181  lcmgcdlem  12218  pcprecl  12430  pc2dvds  12471  4sqlem13m  12544  nninfdclemcl  12608  dfgrp3m  13174  issubg2m  13262  issubgrpd2  13263  issubg3  13265  issubg4m  13266  grpissubg  13267  subgintm  13271  nmzsubg  13283  ghmrn  13330  ghmpreima  13339  dvdsr02  13604  01eq0ring  13688  subrgugrp  13739  lmodfopnelem1  13823  rmodislmodlem  13849  rmodislmod  13850  lss1  13861  lsssubg  13876  islss3  13878  islss4  13881  lss1d  13882  lssintclm  13883  dflidl2rng  13980  lidlsubg  13985  cnsubglem  14078  tgioo  14733  elply2  14914  pw1nct  15563  nninfall  15569  nnnninfen  15581