cdlemk41 - Mathbox for Norm Megill

	Mathbox for Norm Megill	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cdlemk41		Structured version Unicode version

Theorem cdlemk41 34883

Description: Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 19-Jul-2013.)

**Hypothesis**
Ref	Expression
cdlemk41.y	$.\/$ $./\$ $.\/$

**Assertion**
Ref	Expression
cdlemk41	$.\/$ $./\$ $.\/$

Distinct variable groups: $./\$ ,

$.\/$ ,

(

)

(

)

(

)

(

) $.\/$ (

) $./\$ (

)

(

)

(

)

**Proof of Theorem cdlemk41**
Step	Hyp	Ref	Expression
1		nfcvd 2615	. 2 $.\/$ $./\$ $.\/$
2		cdlemk41.y	. . 3 $.\/$ $./\$ $.\/$
3		fveq2 5794	. . . . 5
4	3	oveq2d 6211	. . . 4 $.\/$ $.\/$
5		coeq1 5100	. . . . . 6
6	5	fveq2d 5798	. . . . 5
7	6	oveq2d 6211	. . . 4 $.\/$ $.\/$
8	4, 7	oveq12d 6213	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
9	2, 8	syl5eq 2505	. 2 $.\/$ $./\$ $.\/$
10	1, 9	csbiegf 3414	1 $.\/$ $./\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1370

wcel 1758

csb 3390

ccnv 4942

ccom 4947

cfv 5521 (class class class)co 6195

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1954 ax-ext 2431

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2602 df-rex 2802 df-rab 2805 df-v 3074 df-sbc 3289 df-csb 3391 df-dif 3434 df-un 3436 df-in 3438 df-ss 3445 df-nul 3741 df-if 3895 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4195 df-br 4396 df-opab 4454 df-co 4952 df-iota 5484 df-fv 5529 df-ov 6198

This theorem is referenced by: cdlemkid2 34887 cdlemkfid3N 34888 cdlemky 34889 cdlemk42yN 34907