Theorem elex2 2753

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 2751	. 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 2739

This theorem is referenced by:  snmg  3710  oprcl  3802  brm  4053  ss1o0el1  4197  exss  4227  onintrab2im  4517  regexmidlemm  4531  dmxpid  4848  acexmidlem2  5871  frecabcl  6399  ixpm  6729  enm  6819  ssfilem  6874  fin0  6884  fin0or  6885  diffitest  6886  diffisn  6892  infm  6903  inffiexmid  6905  ctssdc  7111  omct  7115  ctssexmid  7147  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  exmidaclem  7206  caucvgsrlemasr  7788  suplocsrlempr  7805  gtso  8035  sup3exmid  8913  indstr  9592  negm  9614  fzm  10037  fzom  10163  rexfiuz  10997  r19.2uz  11001  resqrexlemgt0  11028  climuni  11300  bezoutlembi  12005  lcmgcdlem  12076  pcprecl  12288  pc2dvds  12328  nninfdclemcl  12448  dfgrp3m  12968  issubg2m  13047  issubgrpd2  13048  issubg3  13050  issubg4m  13051  grpissubg  13052  subgintm  13056  nmzsubg  13068  dvdsr02  13272  01eq0ring  13328  subrgugrp  13359  cnsubglem  13443  tgioo  14016  pw1nct  14722  nninfall  14728