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\in B\to A\in \left\{C,D,A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		idn2	$$⊢\left(A\in B,x=A\to x=A\right)$$
2		3mix3	$$⊢x=A\to \left(x=C\vee x=D\vee x=A\right)$$
3	1 2	e2	$$⊢\left(A\in B,x=A\to \left(x=C\vee x=D\vee x=A\right)\right)$$
4		abid	$$⊢x\in \left\{x|\left(x=C\vee x=D\vee x=A\right)\right\}\leftrightarrow \left(x=C\vee x=D\vee x=A\right)$$
5	3 4	e2bir	$$⊢\left(A\in B,x=A\to x\in \left\{x|\left(x=C\vee x=D\vee x=A\right)\right\}\right)$$
6		dftp2	$$⊢\left\{C,D,A\right\}=\left\{x|\left(x=C\vee x=D\vee x=A\right)\right\}$$
7	6	eleq2i	$$⊢x\in \left\{C,D,A\right\}\leftrightarrow x\in \left\{x|\left(x=C\vee x=D\vee x=A\right)\right\}$$
8	5 7	e2bir	$$⊢\left(A\in B,x=A\to x\in \left\{C,D,A\right\}\right)$$
9		eleq1	$$⊢x=A\to \left(x\in \left\{C,D,A\right\}\leftrightarrow A\in \left\{C,D,A\right\}\right)$$
10	9	biimpd	$$⊢x=A\to \left(x\in \left\{C,D,A\right\}\to A\in \left\{C,D,A\right\}\right)$$
11	1 8 10	e22	$$⊢\left(A\in B,x=A\to A\in \left\{C,D,A\right\}\right)$$
12	11	in2	$$⊢\left(A\in B\to \left(x=A\to A\in \left\{C,D,A\right\}\right)\right)$$
13	12	gen11	$$⊢\left(A\in B\to \forall x\left(x=A\to A\in \left\{C,D,A\right\}\right)\right)$$
14		19.23v	$$⊢\forall x\left(x=A\to A\in \left\{C,D,A\right\}\right)\leftrightarrow \left(\exists xx=A\to A\in \left\{C,D,A\right\}\right)$$
15	13 14	e1bi	$$⊢\left(A\in B\to \left(\exists xx=A\to A\in \left\{C,D,A\right\}\right)\right)$$
16		idn1	$$⊢\left(A\in B\to A\in B\right)$$
17		elisset	$$⊢A\in B\to \exists xx=A$$
18	16 17	e1a	$$⊢\left(A\in B\to \exists xx=A\right)$$
19		id	$$⊢\left(\exists xx=A\to A\in \left\{C,D,A\right\}\right)\to \left(\exists xx=A\to A\in \left\{C,D,A\right\}\right)$$
20	15 18 19	e11	$$⊢\left(A\in B\to A\in \left\{C,D,A\right\}\right)$$
21	20	in1	$$⊢A\in B\to A\in \left\{C,D,A\right\}$$