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