**Description:** A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015)

Ref | Expression | ||
---|---|---|---|

Assertion | prssi | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → { 𝐴 , 𝐵 } ⊆ 𝐶 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | prssg | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ↔ { 𝐴 , 𝐵 } ⊆ 𝐶 ) ) | |

2 | 1 | ibi | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → { 𝐴 , 𝐵 } ⊆ 𝐶 ) |