Theorem eqelssd

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

	Ref	Expression
Hypotheses	eqelssd.1	|- ( ph -> A C_ B )
	eqelssd.2	|- ( ( ph /\ x e. B ) -> x e. A )
Assertion	eqelssd	|- ( ph -> A = B )

Proof

Step	Hyp	Ref	Expression
1		eqelssd.1	|- ( ph -> A C_ B )
2		eqelssd.2	|- ( ( ph /\ x e. B ) -> x e. A )
3	2	ex	|- ( ph -> ( x e. B -> x e. A ) )
4	3	ssrdv	|- ( ph -> B C_ A )
5	1 4	eqssd	|- ( ph -> A = B )