Theorem cdlemk40f

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

	Ref	Expression
Hypotheses	cdlemk40.x	$$⊢X=\left(\iota z\in T|\phi \right)$$
	cdlemk40.u	$$⊢U=\left(g\in T⟼if\left(F=N,g,X\right)\right)$$
Assertion	cdlemk40f	$$⊢\left(F\ne N\wedge G\in T\right)\to U\left(G\right)=⦋G/g⦌X$$

Proof

Step	Hyp	Ref	Expression
1		cdlemk40.x	$$⊢X=\left(\iota z\in T|\phi \right)$$
2		cdlemk40.u	$$⊢U=\left(g\in T⟼if\left(F=N,g,X\right)\right)$$
3	1 2	cdlemk40	$$⊢G\in T\to U\left(G\right)=if\left(F=N,G,⦋G/g⦌X\right)$$
4		ifnefalse	$$⊢F\ne N\to if\left(F=N,G,⦋G/g⦌X\right)=⦋G/g⦌X$$
5	3 4	sylan9eqr	$$⊢\left(F\ne N\wedge G\in T\right)\to U\left(G\right)=⦋G/g⦌X$$