Theorem en3lplem1VD 37302

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

Assertion

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

Distinct variable groups:   x, y, A   x, B, y   x, C, y

Proof of Theorem en3lplem1VD

Step	Hyp	Ref	Expression
1		idn1 37012	. . . . . . 7 |- (. ( A e. B /\ B e. C /\ C e. A ) ->. ( A e. B /\ B e. C /\ C e. A ) ).
2		simp3 1032	. . . . . . 7 |- ( ( A e. B /\ B e. C /\ C e. A ) -> C e. A )
3	1, 2	e1a 37074	. . . . . 6 |- (. ( A e. B /\ B e. C /\ C e. A ) ->. C e. A ).
4		tpid3g 4078	. . . . . 6 |- ( C e. A -> C e. { A , B , C } )
5	3, 4	e1a 37074	. . . . 5 |- (. ( A e. B /\ B e. C /\ C e. A ) ->. C e. { A , B , C } ).
6		idn2 37060	. . . . . 6 |- (. ( A e. B /\ B e. C /\ C e. A ) ,. x = A ->. x = A ).
7		eleq2 2538	. . . . . . 7 |- ( x = A -> ( C e. x <-> C e. A ) )
8	7	biimprd 231	. . . . . 6 |- ( x = A -> ( C e. A -> C e. x ) )
9	6, 3, 8	e21 37180	. . . . 5 |- (. ( A e. B /\ B e. C /\ C e. A ) ,. x = A ->. C e. x ).
10		pm3.2 454	. . . . 5 |- ( C e. { A , B , C } -> ( C e. x -> ( C e. { A , B , C } /\ C e. x ) ) )
11	5, 9, 10	e12 37174	. . . 4 |- (. ( A e. B /\ B e. C /\ C e. A ) ,. x = A ->. ( C e. { A , B , C } /\ C e. x ) ).
12		elex22 3045	. . . 4 |- ( ( C e. { A , B , C } /\ C e. x ) -> E. y ( y e. { A , B , C } /\ y e. x ) )
13	11, 12	e2 37078	. . 3 |- (. ( A e. B /\ B e. C /\ C e. A ) ,. x = A ->. E. y ( y e. { A , B , C } /\ y e. x ) ).
14	13	in2 37052	. 2 |- (. ( A e. B /\ B e. C /\ C e. A ) ->. ( x = A -> E. y ( y e. { A , B , C } /\ y e. x ) ) ).
15	14	in1 37009	1 |- ( ( A e. B /\ B e. C /\ C e. A ) -> ( x = A -> E. y ( y e. { A , B , C } /\ y e. x ) ) )

Syntax hints:   -> wi 4   /\ wa 376   /\ w3a 1007   = wceq 1452   E.wex 1671   e. wcel 1904   {ctp 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-un 3395  df-sn 3960  df-pr 3962  df-tp 3964  df-vd1 37008  df-vd2 37016

This theorem is referenced by:  en3lplem2VD  37303