Metamath Proof Explorer


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 ABxxB

Proof

Step Hyp Ref Expression
1 idn1 ABAB
2 idn2 AB,x=Ax=A
3 eleq1a ABx=AxB
4 1 2 3 e12 AB,x=AxB
5 4 in2 ABx=AxB
6 5 gen11 ABxx=AxB
7 elisset ABxx=A
8 1 7 e1a ABxx=A
9 exim xx=AxBxx=AxxB
10 6 8 9 e11 ABxxB
11 10 in1 ABxxB