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	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
	parhomideq.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
	parhomideq.e	⊢ ( 𝜑 → 𝑈 = 𝑉 )
	parhomideq2.s	⊢ 𝑆 ∈ V
	parhomideq2.j	⊢ 𝐽 ∈ V
	parhomideq2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
	parhomideq2.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
Assertion	parhomideq2	⊢ ( 𝜑 → 𝐹 = 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2		parhomideq.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
3		parhomideq.e	⊢ ( 𝜑 → 𝑈 = 𝑉 )
4		parhomideq2.s	⊢ 𝑆 ∈ V
5		parhomideq2.j	⊢ 𝐽 ∈ V
6		parhomideq2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
7		parhomideq2.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
8	1 4	parhomval	⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝑈 𝐻 𝑉 ) = if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) )
9	6 7 8	syl2anc	⊢ ( 𝜑 → ( 𝑈 𝐻 𝑉 ) = if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) )
10	3	iftrued	⊢ ( 𝜑 → if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) = { 𝐽 } )
11	9 10	eqtrd	⊢ ( 𝜑 → ( 𝑈 𝐻 𝑉 ) = { 𝐽 } )
12	2 11	eleqtrd	⊢ ( 𝜑 → 𝐹 ∈ { 𝐽 } )
13	12	elsnd	⊢ ( 𝜑 → 𝐹 = 𝐽 )