Theorem parhomideq2

Description: Variant of parhomideq . (Contributed by Zhi Wang, 14-Sep-2026) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	parhomval.h	|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
	parhomideq.f	|- ( ph -> F e. ( U H V ) )
	parhomideq.e	|- ( ph -> U = V )
	parhomideq2.s	|- S e. _V
	parhomideq2.j	|- J e. _V
	parhomideq2.u	|- ( ph -> U e. B )
	parhomideq2.v	|- ( ph -> V e. B )
Assertion	parhomideq2	|- ( ph -> F = J )

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
2		parhomideq.f	|- ( ph -> F e. ( U H V ) )
3		parhomideq.e	|- ( ph -> U = V )
4		parhomideq2.s	|- S e. _V
5		parhomideq2.j	|- J e. _V
6		parhomideq2.u	|- ( ph -> U e. B )
7		parhomideq2.v	|- ( ph -> V e. B )
8	1 4	parhomval	|- ( ( U e. B /\ V e. B ) -> ( U H V ) = if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) )
9	6 7 8	syl2anc	|- ( ph -> ( U H V ) = if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) )
10	3	iftrued	|- ( ph -> if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) = { J } )
11	9 10	eqtrd	|- ( ph -> ( U H V ) = { J } )
12	2 11	eleqtrd	|- ( ph -> F e. { J } )
13	12	elsnd	|- ( ph -> F = J )