**Description:** Equality deduction from two subclass relationships. Compare Theorem 4
of Suppes p. 22. (Contributed by NM, 27-Jun-2004)

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

Hypotheses | eqssd.1 | $${\u22a2}{\phi}\to {A}\subseteq {B}$$ | |

eqssd.2 | $${\u22a2}{\phi}\to {B}\subseteq {A}$$ | ||

Assertion | eqssd | $${\u22a2}{\phi}\to {A}={B}$$ |

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

1 | eqssd.1 | $${\u22a2}{\phi}\to {A}\subseteq {B}$$ | |

2 | eqssd.2 | $${\u22a2}{\phi}\to {B}\subseteq {A}$$ | |

3 | eqss | $${\u22a2}{A}={B}\leftrightarrow \left({A}\subseteq {B}\wedge {B}\subseteq {A}\right)$$ | |

4 | 1 2 3 | sylanbrc | $${\u22a2}{\phi}\to {A}={B}$$ |