Theorem elex2 2754

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 2249	. . 3 |- ( A e. B -> ( x = A -> x e. B ) )
2	1	alrimiv 1874	. 2 |- ( A e. B -> A. x ( x = A -> x e. B ) )
3		elisset 2752	. 2 |- ( A e. B -> E. x x = A )
4		exim 1599	. 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 1351   = wceq 1353   E.wex 1492   e. wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2740

This theorem is referenced by:  snmg  3711  oprcl  3803  brm  4054  ss1o0el1  4198  exss  4228  onintrab2im  4518  regexmidlemm  4532  dmxpid  4849  acexmidlem2  5872  frecabcl  6400  ixpm  6730  enm  6820  ssfilem  6875  fin0  6885  fin0or  6886  diffitest  6887  diffisn  6893  infm  6904  inffiexmid  6906  ctssdc  7112  omct  7116  ctssexmid  7148  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  exmidaclem  7207  caucvgsrlemasr  7789  suplocsrlempr  7806  gtso  8036  sup3exmid  8914  indstr  9593  negm  9615  fzm  10038  fzom  10164  rexfiuz  10998  r19.2uz  11002  resqrexlemgt0  11029  climuni  11301  bezoutlembi  12006  lcmgcdlem  12077  pcprecl  12289  pc2dvds  12329  nninfdclemcl  12449  dfgrp3m  12969  issubg2m  13049  issubgrpd2  13050  issubg3  13052  issubg4m  13053  grpissubg  13054  subgintm  13058  nmzsubg  13070  dvdsr02  13274  01eq0ring  13330  subrgugrp  13361  lmodfopnelem1  13414  rmodislmodlem  13440  rmodislmod  13441  cnsubglem  13476  tgioo  14049  pw1nct  14755  nninfall  14761