This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdlemk40f

Description: TODO: fix comment. (Contributed by NM, 31-Jul-2013)

Ref Expression
Hypotheses cdlemk40.x ⊢ X = ι z ∈ T | φ
cdlemk40.u ⊢ U = g ∈ T ⟼ if F = N g X
Assertion cdlemk40f ⊢ F ≠ N ∧ G ∈ T → U ⁡ G = ⦋ G / g⦌ X

Proof

Step Hyp Ref Expression
1 cdlemk40.x ⊢ X = ι z ∈ T | φ
2 cdlemk40.u ⊢ U = g ∈ T ⟼ if F = N g X
3 1 2 cdlemk40 ⊢ G ∈ T → U ⁡ G = if F = N G ⦋ G / g⦌ X
4 ifnefalse ⊢ F ≠ N → if F = N G ⦋ G / g⦌ X = ⦋ G / g⦌ X
5 3 4 sylan9eqr ⊢ F ≠ N ∧ G ∈ T → U ⁡ G = ⦋ G / g⦌ X