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 } )