**Description:** Deduction version of prssi : A pair of elements of a class is a
subset of the class. (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Hypotheses | prssd.1 | $${\u22a2}{\phi}\to {A}\in {C}$$ | |

prssd.2 | $${\u22a2}{\phi}\to {B}\in {C}$$ | ||

Assertion | prssd | $${\u22a2}{\phi}\to \left\{{A},{B}\right\}\subseteq {C}$$ |

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

1 | prssd.1 | $${\u22a2}{\phi}\to {A}\in {C}$$ | |

2 | prssd.2 | $${\u22a2}{\phi}\to {B}\in {C}$$ | |

3 | prssi | $${\u22a2}\left({A}\in {C}\wedge {B}\in {C}\right)\to \left\{{A},{B}\right\}\subseteq {C}$$ | |

4 | 1 2 3 | syl2anc | $${\u22a2}{\phi}\to \left\{{A},{B}\right\}\subseteq {C}$$ |