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  3801  brm  4051  ss1o0el1  4195  exss  4225  onintrab2im  4515  regexmidlemm  4529  dmxpid  4845  acexmidlem2  5867  frecabcl  6395  ixpm  6725  enm  6815  ssfilem  6870  fin0  6880  fin0or  6881  diffitest  6882  diffisn  6888  infm  6899  inffiexmid  6901  ctssdc  7107  omct  7111  ctssexmid  7143  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  exmidaclem  7202  caucvgsrlemasr  7784  suplocsrlempr  7801  gtso  8030  sup3exmid  8908  indstr  9587  negm  9609  fzm  10031  fzom  10157  rexfiuz  10989  r19.2uz  10993  resqrexlemgt0  11020  climuni  11292  bezoutlembi  11996  lcmgcdlem  12067  pcprecl  12279  pc2dvds  12319  nninfdclemcl  12439  dfgrp3m  12897  issubg2m  12975  issubgrpd2  12976  issubg3  12978  issubg4m  12979  grpissubg  12980  subgintm  12984  dvdsr02  13173  01eq0ring  13229  tgioo  13828  pw1nct  14523  nninfall  14529