Description: Closed theorem form of tpid2 . (Contributed by Glauco Siliprandi, 23-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | tpid2g | |- ( A e. B -> A e. { C , A , D } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |- A = A |
|
2 | 1 | 3mix2i | |- ( A = C \/ A = A \/ A = D ) |
3 | eltpg | |- ( A e. B -> ( A e. { C , A , D } <-> ( A = C \/ A = A \/ A = D ) ) ) |
|
4 | 2 3 | mpbiri | |- ( A e. B -> A e. { C , A , D } ) |