This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tpss

Description: An unordered triple of elements of a class is a subset of the class. (Contributed by NM, 9-Apr-1994) (Proof shortened by Andrew Salmon, 29-Jun-2011)

		Ref	Expression
	Hypotheses	tpss.1	⊢ 𝐴 ∈ V
		tpss.2	⊢ 𝐵 ∈ V
		tpss.3	⊢ 𝐶 ∈ V
	Assertion	tpss	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) ↔ { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		tpss.1	⊢ 𝐴 ∈ V
2		tpss.2	⊢ 𝐵 ∈ V
3		tpss.3	⊢ 𝐶 ∈ V
4		unss	⊢ ( ( { 𝐴 , 𝐵 } ⊆ 𝐷 ∧ { 𝐶 } ⊆ 𝐷 ) ↔ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ⊆ 𝐷 )
5		df-3an	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) ↔ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐶 ∈ 𝐷 ) )
6	1 2	prss	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ) ↔ { 𝐴 , 𝐵 } ⊆ 𝐷 )
7	3	snss	⊢ ( 𝐶 ∈ 𝐷 ↔ { 𝐶 } ⊆ 𝐷 )
8	6 7	anbi12i	⊢ ( ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐶 ∈ 𝐷 ) ↔ ( { 𝐴 , 𝐵 } ⊆ 𝐷 ∧ { 𝐶 } ⊆ 𝐷 ) )
9	5 8	bitri	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) ↔ ( { 𝐴 , 𝐵 } ⊆ 𝐷 ∧ { 𝐶 } ⊆ 𝐷 ) )
10		df-tp	⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
11	10	sseq1i	⊢ ( { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 ↔ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ⊆ 𝐷 )
12	4 9 11	3bitr4i	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) ↔ { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )