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 37043

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 2617	. 2 $.\/$ $./\$ $.\/$
2		cdlemk41.y	. . 3 $.\/$ $./\$ $.\/$
3		fveq2 5848	. . . . 5
4	3	oveq2d 6286	. . . 4 $.\/$ $.\/$
5		coeq1 5149	. . . . . 6
6	5	fveq2d 5852	. . . . 5
7	6	oveq2d 6286	. . . 4 $.\/$ $.\/$
8	4, 7	oveq12d 6288	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
9	2, 8	syl5eq 2507	. 2 $.\/$ $./\$ $.\/$
10	1, 9	csbiegf 3444	1 $.\/$ $./\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1398

wcel 1823

csb 3420

ccnv 4987

ccom 4992

cfv 5570 (class class class)co 6270

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-rex 2810 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-nul 3784 df-if 3930 df-sn 4017 df-pr 4019 df-op 4023 df-uni 4236 df-br 4440 df-opab 4498 df-co 4997 df-iota 5534 df-fv 5578 df-ov 6273

This theorem is referenced by: cdlemkid2 37047 cdlemkfid3N 37048 cdlemky 37049 cdlemk42yN 37067