Theorem elex2 2779

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 2268	. . 3 |- ( A e. B -> ( x = A -> x e. B ) )
2	1	alrimiv 1888	. 2 |- ( A e. B -> A. x ( x = A -> x e. B ) )
3		elisset 2777	. 2 |- ( A e. B -> E. x x = A )
4		exim 1613	. 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 1506   e. wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765

This theorem is referenced by:  snmg  3741  oprcl  3833  brm  4084  ss1o0el1  4231  exss  4261  onintrab2im  4555  regexmidlemm  4569  dmxpid  4888  acexmidlem2  5922  frecabcl  6466  ixpm  6798  enm  6888  ssfilem  6945  fin0  6955  fin0or  6956  diffitest  6957  diffisn  6963  infm  6974  inffiexmid  6976  ctssdc  7188  omct  7192  ctssexmid  7225  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  acnrcl  7284  exmidaclem  7291  caucvgsrlemasr  7874  suplocsrlempr  7891  gtso  8122  sup3exmid  9001  indstr  9684  negm  9706  fzm  10130  fzom  10257  rexfiuz  11171  r19.2uz  11175  resqrexlemgt0  11202  climuni  11475  bezoutlembi  12197  nninfct  12233  lcmgcdlem  12270  pcprecl  12483  pc2dvds  12524  4sqlem13m  12597  nninfdclemcl  12690  dfgrp3m  13301  issubg2m  13395  issubgrpd2  13396  issubg3  13398  issubg4m  13399  grpissubg  13400  subgintm  13404  nmzsubg  13416  ghmrn  13463  ghmpreima  13472  dvdsr02  13737  01eq0ring  13821  subrgugrp  13872  lmodfopnelem1  13956  rmodislmodlem  13982  rmodislmod  13983  lss1  13994  lsssubg  14009  islss3  14011  islss4  14014  lss1d  14015  lssintclm  14016  dflidl2rng  14113  lidlsubg  14118  cnsubglem  14211  tgioo  14874  elply2  15055  pw1nct  15734  nninfall  15740  nnnninfen  15752