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 34399

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 2570	. 2 $.\/$ $./\$ $.\/$
2		cdlemk41.y	. . 3 $.\/$ $./\$ $.\/$
3		fveq2 5825	. . . . 5
4	3	oveq2d 6265	. . . 4 $.\/$ $.\/$
5		coeq1 4954	. . . . . 6
6	5	fveq2d 5829	. . . . 5
7	6	oveq2d 6265	. . . 4 $.\/$ $.\/$
8	4, 7	oveq12d 6267	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
9	2, 8	syl5eq 2474	. 2 $.\/$ $./\$ $.\/$
10	1, 9	csbiegf 3362	1 $.\/$ $./\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1437

wcel 1872

csb 3338

ccnv 4795

ccom 4800

cfv 5544 (class class class)co 6249

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2063 ax-ext 2408

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3an 984 df-tru 1440 df-ex 1658 df-nf 1662 df-sb 1791 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2558 df-rex 2720 df-rab 2723 df-v 3024 df-sbc 3243 df-csb 3339 df-dif 3382 df-un 3384 df-in 3386 df-ss 3393 df-nul 3705 df-if 3855 df-sn 3942 df-pr 3944 df-op 3948 df-uni 4163 df-br 4367 df-opab 4426 df-co 4805 df-iota 5508 df-fv 5552 df-ov 6252

This theorem is referenced by: cdlemkid2 34403 cdlemkfid3N 34404 cdlemky 34405 cdlemk42yN 34423