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	⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ { 𝐶 , 𝐷 , 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		idn2	⊢ (    𝐴 ∈ 𝐵    ,    𝑥 = 𝐴    ▶    𝑥 = 𝐴    )
2		3mix3	⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴 ) )
3	1 2	e2	⊢ (    𝐴 ∈ 𝐵    ,    𝑥 = 𝐴    ▶    ( 𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴 )    )
4		abid	⊢ ( 𝑥 ∈ { 𝑥 ∣ ( 𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴 ) } ↔ ( 𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴 ) )
5	3 4	e2bir	⊢ (    𝐴 ∈ 𝐵    ,    𝑥 = 𝐴    ▶    𝑥 ∈ { 𝑥 ∣ ( 𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴 ) }    )
6		dftp2	⊢ { 𝐶 , 𝐷 , 𝐴 } = { 𝑥 ∣ ( 𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴 ) }
7	6	eleq2i	⊢ ( 𝑥 ∈ { 𝐶 , 𝐷 , 𝐴 } ↔ 𝑥 ∈ { 𝑥 ∣ ( 𝑥 = 𝐶 ∨ 𝑥 = 𝐷 ∨ 𝑥 = 𝐴 ) } )
8	5 7	e2bir	⊢ (    𝐴 ∈ 𝐵    ,    𝑥 = 𝐴    ▶    𝑥 ∈ { 𝐶 , 𝐷 , 𝐴 }    )
9		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ { 𝐶 , 𝐷 , 𝐴 } ↔ 𝐴 ∈ { 𝐶 , 𝐷 , 𝐴 } ) )
10	9	biimpd	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ { 𝐶 , 𝐷 , 𝐴 } → 𝐴 ∈ { 𝐶 , 𝐷 , 𝐴 } ) )
11	1 8 10	e22	⊢ (    𝐴 ∈ 𝐵    ,    𝑥 = 𝐴    ▶    𝐴 ∈ { 𝐶 , 𝐷 , 𝐴 }    )
12	11	in2	⊢ (    𝐴 ∈ 𝐵    ▶    ( 𝑥 = 𝐴 → 𝐴 ∈ { 𝐶 , 𝐷 , 𝐴 } )    )
13	12	gen11	⊢ (    𝐴 ∈ 𝐵    ▶    ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐴 ∈ { 𝐶 , 𝐷 , 𝐴 } )    )
14		19.23v	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐴 ∈ { 𝐶 , 𝐷 , 𝐴 } ) ↔ ( ∃ 𝑥 𝑥 = 𝐴 → 𝐴 ∈ { 𝐶 , 𝐷 , 𝐴 } ) )
15	13 14	e1bi	⊢ (    𝐴 ∈ 𝐵    ▶    ( ∃ 𝑥 𝑥 = 𝐴 → 𝐴 ∈ { 𝐶 , 𝐷 , 𝐴 } )    )
16		idn1	⊢ (    𝐴 ∈ 𝐵    ▶    𝐴 ∈ 𝐵    )
17		elisset	⊢ ( 𝐴 ∈ 𝐵 → ∃ 𝑥 𝑥 = 𝐴 )
18	16 17	e1a	⊢ (    𝐴 ∈ 𝐵    ▶    ∃ 𝑥 𝑥 = 𝐴    )
19		id	⊢ ( ( ∃ 𝑥 𝑥 = 𝐴 → 𝐴 ∈ { 𝐶 , 𝐷 , 𝐴 } ) → ( ∃ 𝑥 𝑥 = 𝐴 → 𝐴 ∈ { 𝐶 , 𝐷 , 𝐴 } ) )
20	15 18 19	e11	⊢ (    𝐴 ∈ 𝐵    ▶    𝐴 ∈ { 𝐶 , 𝐷 , 𝐴 }    )
21	20	in1	⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ { 𝐶 , 𝐷 , 𝐴 } )