Metamath Proof Explorer

Theorem tpssg

Description: An unordered triple of elements of a class is a subset of the class. (Contributed by Thierry Arnoux, 2-Nov-2025)

Ref Expression
Assertion tpssg ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → A ∈ D ∧ B ∈ D ∧ C ∈ D ↔ A B C ⊆ D

Proof

Step Hyp Ref Expression
1 df-3an ⊢ A ∈ D ∧ B ∈ D ∧ C ∈ D ↔ A ∈ D ∧ B ∈ D ∧ C ∈ D
2 prssg ⊢ A ∈ V ∧ B ∈ W → A ∈ D ∧ B ∈ D ↔ A B ⊆ D
3 snssg ⊢ C ∈ X → C ∈ D ↔ C ⊆ D
4 2 3 bi2anan9 ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → A ∈ D ∧ B ∈ D ∧ C ∈ D ↔ A B ⊆ D ∧ C ⊆ D
5 unss ⊢ A B ⊆ D ∧ C ⊆ D ↔ A B ∪ C ⊆ D
6 df-tp ⊢ A B C = A B ∪ C
7 6 sseq1i ⊢ A B C ⊆ D ↔ A B ∪ C ⊆ D
8 5 7 bitr4i ⊢ A B ⊆ D ∧ C ⊆ D ↔ A B C ⊆ D
9 4 8 bitrdi ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → A ∈ D ∧ B ∈ D ∧ C ∈ D ↔ A B C ⊆ D
10 1 9 bitrid ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → A ∈ D ∧ B ∈ D ∧ C ∈ D ↔ A B C ⊆ D
11 10 3impa ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → A ∈ D ∧ B ∈ D ∧ C ∈ D ↔ A B C ⊆ D