Metamath Proof Explorer

Theorem en3lplem1VD

Description: Virtual deduction proof of en3lplem1 . (Contributed by Alan Sare, 24-Oct-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion en3lplem1VD 
|- ( ( A e. B /\ B e. C /\ C e. A ) -> ( x = A -> E. y ( y e. { A , B , C } /\ y e. x ) ) )

Proof

Step Hyp Ref Expression
1 idn1 
 |-  (. ( A e. B /\ B e. C /\ C e. A ) ->. ( A e. B /\ B e. C /\ C e. A ) ).
2 simp3 
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> C e. A )
3 1 2 e1a 
 |-  (. ( A e. B /\ B e. C /\ C e. A ) ->. C e. A ).
4 tpid3g 
 |-  ( C e. A -> C e. { A , B , C } )
5 3 4 e1a 
 |-  (. ( A e. B /\ B e. C /\ C e. A ) ->. C e. { A , B , C } ).
6 idn2 
 |-  (. ( A e. B /\ B e. C /\ C e. A ) ,. x = A ->. x = A ).
7 eleq2 
 |-  ( x = A -> ( C e. x <-> C e. A ) )
8 7 biimprd 
 |-  ( x = A -> ( C e. A -> C e. x ) )
9 6 3 8 e21 
 |-  (. ( A e. B /\ B e. C /\ C e. A ) ,. x = A ->. C e. x ).
10 pm3.2 
 |-  ( C e. { A , B , C } -> ( C e. x -> ( C e. { A , B , C } /\ C e. x ) ) )
11 5 9 10 e12 
 |-  (. ( A e. B /\ B e. C /\ C e. A ) ,. x = A ->. ( C e. { A , B , C } /\ C e. x ) ).
12 elex22 
 |-  ( ( C e. { A , B , C } /\ C e. x ) -> E. y ( y e. { A , B , C } /\ y e. x ) )
13 11 12 e2 
 |-  (. ( A e. B /\ B e. C /\ C e. A ) ,. x = A ->. E. y ( y e. { A , B , C } /\ y e. x ) ).
14 13 in2 
 |-  (. ( A e. B /\ B e. C /\ C e. A ) ->. ( x = A -> E. y ( y e. { A , B , C } /\ y e. x ) ) ).
15 14 in1 
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x = A -> E. y ( y e. { A , B , C } /\ y e. x ) ) )