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 = ( BaseSet ` U )
	ip2eqi.7	|- P = ( .iOLD ` U )
	ip2eqi.u	|- U e. CPreHilOLD
Assertion	phoeqi	|- ( ( S : Y --> X /\ T : Y --> X ) -> ( A. x e. X A. y e. Y ( x P ( S ` y ) ) = ( x P ( T ` y ) ) <-> S = T ) )

Proof

Step	Hyp	Ref	Expression
1		ip2eqi.1	|- X = ( BaseSet ` U )
2		ip2eqi.7	|- P = ( .iOLD ` U )
3		ip2eqi.u	|- U e. CPreHilOLD
4		ralcom	|- ( A. x e. X A. y e. Y ( x P ( S ` y ) ) = ( x P ( T ` y ) ) <-> A. y e. Y A. x e. X ( x P ( S ` y ) ) = ( x P ( T ` y ) ) )
5		ffvelcdm	|- ( ( S : Y --> X /\ y e. Y ) -> ( S ` y ) e. X )
6		ffvelcdm	|- ( ( T : Y --> X /\ y e. Y ) -> ( T ` y ) e. X )
7	1 2 3	ip2eqi	|- ( ( ( S ` y ) e. X /\ ( T ` y ) e. X ) -> ( A. x e. X ( x P ( S ` y ) ) = ( x P ( T ` y ) ) <-> ( S ` y ) = ( T ` y ) ) )
8	5 6 7	syl2an	|- ( ( ( S : Y --> X /\ y e. Y ) /\ ( T : Y --> X /\ y e. Y ) ) -> ( A. x e. X ( x P ( S ` y ) ) = ( x P ( T ` y ) ) <-> ( S ` y ) = ( T ` y ) ) )
9	8	anandirs	|- ( ( ( S : Y --> X /\ T : Y --> X ) /\ y e. Y ) -> ( A. x e. X ( x P ( S ` y ) ) = ( x P ( T ` y ) ) <-> ( S ` y ) = ( T ` y ) ) )
10	9	ralbidva	|- ( ( S : Y --> X /\ T : Y --> X ) -> ( A. y e. Y A. x e. X ( x P ( S ` y ) ) = ( x P ( T ` y ) ) <-> A. y e. Y ( S ` y ) = ( T ` y ) ) )
11		ffn	|- ( S : Y --> X -> S Fn Y )
12		ffn	|- ( T : Y --> X -> T Fn Y )
13		eqfnfv	|- ( ( S Fn Y /\ T Fn Y ) -> ( S = T <-> A. y e. Y ( S ` y ) = ( T ` y ) ) )
14	11 12 13	syl2an	|- ( ( S : Y --> X /\ T : Y --> X ) -> ( S = T <-> A. y e. Y ( S ` y ) = ( T ` y ) ) )
15	10 14	bitr4d	|- ( ( S : Y --> X /\ T : Y --> X ) -> ( A. y e. Y A. x e. X ( x P ( S ` y ) ) = ( x P ( T ` y ) ) <-> S = T ) )
16	4 15	bitrid	|- ( ( S : Y --> X /\ T : Y --> X ) -> ( A. x e. X A. y e. Y ( x P ( S ` y ) ) = ( x P ( T ` y ) ) <-> S = T ) )