Theorem eqelssd

Description: Equality deduction from subclass relationship and membership. (Contributed by AV, 21-Aug-2022)

	Ref	Expression
Hypotheses	eqelssd.1	$$⊢\phi \to A\subseteq B$$
	eqelssd.2	$$⊢\left(\phi \wedge x\in B\right)\to x\in A$$
Assertion	eqelssd	$$⊢\phi \to A=B$$

Proof

Step	Hyp	Ref	Expression
1		eqelssd.1	$$⊢\phi \to A\subseteq B$$
2		eqelssd.2	$$⊢\left(\phi \wedge x\in B\right)\to x\in A$$
3	2	ex	$$⊢\phi \to \left(x\in B\to x\in A\right)$$
4	3	ssrdv	$$⊢\phi \to B\subseteq A$$
5	1 4	eqssd	$$⊢\phi \to A=B$$