Metamath Proof Explorer

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 ∈ B , y ∈ B ⟼ if x = y J if x = X ∧ y = Y S ∅
parhomideq.f ⊢ φ → F ∈ U H V
parhomideq.e ⊢ φ → U = V
parhomideq2.s ⊢ S ∈ V
parhomideq2.j ⊢ J ∈ V
parhomideq2.u ⊢ φ → U ∈ B
parhomideq2.v ⊢ φ → V ∈ B
Assertion parhomideq2 ⊢ φ → F = J

Proof

Step Hyp Ref Expression
1 parhomval.h ⊢ H = x ∈ B , y ∈ B ⟼ if x = y J if x = X ∧ y = Y S ∅
2 parhomideq.f ⊢ φ → F ∈ U H V
3 parhomideq.e ⊢ φ → U = V
4 parhomideq2.s ⊢ S ∈ V
5 parhomideq2.j ⊢ J ∈ V
6 parhomideq2.u ⊢ φ → U ∈ B
7 parhomideq2.v ⊢ φ → V ∈ B
8 1 4 parhomval ⊢ U ∈ B ∧ V ∈ B → U H V = if U = V J if U = X ∧ V = Y S ∅
9 6 7 8 syl2anc ⊢ φ → U H V = if U = V J if U = X ∧ V = Y S ∅
10 3 iftrued ⊢ φ → if U = V J if U = X ∧ V = Y S ∅ = J
11 9 10 eqtrd ⊢ φ → U H V = J
12 2 11 eleqtrd ⊢ φ → F ∈ J
13 12 elsnd ⊢ φ → F = J