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\in B\to \exists xx\in B$$

Proof

Step	Hyp	Ref	Expression
1		idn1	$$⊢\left(A\in B\to A\in B\right)$$
2		idn2	$$⊢\left(A\in B,x=A\to x=A\right)$$
3		eleq1a	$$⊢A\in B\to \left(x=A\to x\in B\right)$$
4	1 2 3	e12	$$⊢\left(A\in B,x=A\to x\in B\right)$$
5	4	in2	$$⊢\left(A\in B\to \left(x=A\to x\in B\right)\right)$$
6	5	gen11	$$⊢\left(A\in B\to \forall x\left(x=A\to x\in B\right)\right)$$
7		elisset	$$⊢A\in B\to \exists xx=A$$
8	1 7	e1a	$$⊢\left(A\in B\to \exists xx=A\right)$$
9		exim	$$⊢\forall x\left(x=A\to x\in B\right)\to \left(\exists xx=A\to \exists xx\in B\right)$$
10	6 8 9	e11	$$⊢\left(A\in B\to \exists xx\in B\right)$$
11	10	in1	$$⊢A\in B\to \exists xx\in B$$