Theorem phoeqi

Description: A condition implying that two operators are equal. (Contributed by NM, 25-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ip2eqi.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	ip2eqi.7	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
	ip2eqi.u	$$⊢U\in {CPreHil}_{\mathrm{OLD}}$$
Assertion	phoeqi	$$⊢\left(S:Y⟶X\wedge T:Y⟶X\right)\to \left(\forall x\in X\forall y\in YxPS\left(y\right)=xPT\left(y\right)\leftrightarrow S=T\right)$$

Proof

Step	Hyp	Ref	Expression
1		ip2eqi.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		ip2eqi.7	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
3		ip2eqi.u	$$⊢U\in {CPreHil}_{\mathrm{OLD}}$$
4		ralcom	$$⊢\forall x\in X\forall y\in YxPS\left(y\right)=xPT\left(y\right)\leftrightarrow \forall y\in Y\forall x\in XxPS\left(y\right)=xPT\left(y\right)$$
5		ffvelcdm	$$⊢\left(S:Y⟶X\wedge y\in Y\right)\to S\left(y\right)\in X$$
6		ffvelcdm	$$⊢\left(T:Y⟶X\wedge y\in Y\right)\to T\left(y\right)\in X$$
7	1 2 3	ip2eqi	$$⊢\left(S\left(y\right)\in X\wedge T\left(y\right)\in X\right)\to \left(\forall x\in XxPS\left(y\right)=xPT\left(y\right)\leftrightarrow S\left(y\right)=T\left(y\right)\right)$$
8	5 6 7	syl2an	$$⊢\left(\left(S:Y⟶X\wedge y\in Y\right)\wedge \left(T:Y⟶X\wedge y\in Y\right)\right)\to \left(\forall x\in XxPS\left(y\right)=xPT\left(y\right)\leftrightarrow S\left(y\right)=T\left(y\right)\right)$$
9	8	anandirs	$$⊢\left(\left(S:Y⟶X\wedge T:Y⟶X\right)\wedge y\in Y\right)\to \left(\forall x\in XxPS\left(y\right)=xPT\left(y\right)\leftrightarrow S\left(y\right)=T\left(y\right)\right)$$
10	9	ralbidva	$$⊢\left(S:Y⟶X\wedge T:Y⟶X\right)\to \left(\forall y\in Y\forall x\in XxPS\left(y\right)=xPT\left(y\right)\leftrightarrow \forall y\in YS\left(y\right)=T\left(y\right)\right)$$
11		ffn	$$⊢S:Y⟶X\to SFnY$$
12		ffn	$$⊢T:Y⟶X\to TFnY$$
13		eqfnfv	$$⊢\left(SFnY\wedge TFnY\right)\to \left(S=T\leftrightarrow \forall y\in YS\left(y\right)=T\left(y\right)\right)$$
14	11 12 13	syl2an	$$⊢\left(S:Y⟶X\wedge T:Y⟶X\right)\to \left(S=T\leftrightarrow \forall y\in YS\left(y\right)=T\left(y\right)\right)$$
15	10 14	bitr4d	$$⊢\left(S:Y⟶X\wedge T:Y⟶X\right)\to \left(\forall y\in Y\forall x\in XxPS\left(y\right)=xPT\left(y\right)\leftrightarrow S=T\right)$$
16	4 15	bitrid	$$⊢\left(S:Y⟶X\wedge T:Y⟶X\right)\to \left(\forall x\in X\forall y\in YxPS\left(y\right)=xPT\left(y\right)\leftrightarrow S=T\right)$$