Metamath Proof Explorer

Theorem tpid3gVD

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

Ref Expression
Assertion tpid3gVD 
|- ( A e. B -> A e. { C , D , A } )

Proof

Step Hyp Ref Expression
1 idn2 
 |-  (. A e. B ,. x = A ->. x = A ).
2 3mix3 
 |-  ( x = A -> ( x = C \/ x = D \/ x = A ) )
3 1 2 e2 
 |-  (. A e. B ,. x = A ->. ( x = C \/ x = D \/ x = A ) ).
4 abid 
 |-  ( x e. { x | ( x = C \/ x = D \/ x = A ) } <-> ( x = C \/ x = D \/ x = A ) )
5 3 4 e2bir 
 |-  (. A e. B ,. x = A ->. x e. { x | ( x = C \/ x = D \/ x = A ) } ).
6 dftp2 
 |-  { C , D , A } = { x | ( x = C \/ x = D \/ x = A ) }
7 6 eleq2i 
 |-  ( x e. { C , D , A } <-> x e. { x | ( x = C \/ x = D \/ x = A ) } )
8 5 7 e2bir 
 |-  (. A e. B ,. x = A ->. x e. { C , D , A } ).
9 eleq1 
 |-  ( x = A -> ( x e. { C , D , A } <-> A e. { C , D , A } ) )
10 9 biimpd 
 |-  ( x = A -> ( x e. { C , D , A } -> A e. { C , D , A } ) )
11 1 8 10 e22 
 |-  (. A e. B ,. x = A ->. A e. { C , D , A } ).
12 11 in2 
 |-  (. A e. B ->. ( x = A -> A e. { C , D , A } ) ).
13 12 gen11 
 |-  (. A e. B ->. A. x ( x = A -> A e. { C , D , A } ) ).
14 19.23v 
 |-  ( A. x ( x = A -> A e. { C , D , A } ) <-> ( E. x x = A -> A e. { C , D , A } ) )
15 13 14 e1bi 
 |-  (. A e. B ->. ( E. x x = A -> A e. { C , D , A } ) ).
16 idn1 
 |-  (. A e. B ->. A e. B ).
17 elisset 
 |-  ( A e. B -> E. x x = A )
18 16 17 e1a 
 |-  (. A e. B ->. E. x x = A ).
19 id 
 |-  ( ( E. x x = A -> A e. { C , D , A } ) -> ( E. x x = A -> A e. { C , D , A } ) )
20 15 18 19 e11 
 |-  (. A e. B ->. A e. { C , D , A } ).
21 20 in1 
 |-  ( A e. B -> A e. { C , D , A } )