Theorem elex2VD

Description: Virtual deduction proof of elex2 . (Contributed by Alan Sare, 25-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	elex2VD	|- ( A e. B -> E. x x e. B )

Proof

Step	Hyp	Ref	Expression
1		idn1	|- (. A e. B ->. A e. B ).
2		idn2	|- (. A e. B ,. x = A ->. x = A ).
3		eleq1a	|- ( A e. B -> ( x = A -> x e. B ) )
4	1 2 3	e12	|- (. A e. B ,. x = A ->. x e. B ).
5	4	in2	|- (. A e. B ->. ( x = A -> x e. B ) ).
6	5	gen11	|- (. A e. B ->. A. x ( x = A -> x e. B ) ).
7		elisset	|- ( A e. B -> E. x x = A )
8	1 7	e1a	|- (. A e. B ->. E. x x = A ).
9		exim	|- ( A. x ( x = A -> x e. B ) -> ( E. x x = A -> E. x x e. B ) )
10	6 8 9	e11	|- (. A e. B ->. E. x x e. B ).
11	10	in1	|- ( A e. B -> E. x x e. B )