Theorem cdleme31sc 41218

Description: Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.)

Hypotheses

Ref	Expression
cdleme31sc.c	⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)))
cdleme31sc.x	⊢ 𝑋 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊)))

Assertion

Ref	Expression
cdleme31sc	⊢ (𝑅 ∈ 𝐴 → ⦋𝑅 / 𝑠⦌𝐶 = 𝑋)

Distinct variable groups:   𝐴,𝑠   ∨ ,𝑠   ∧ ,𝑠   𝑃,𝑠   𝑄,𝑠   𝑅,𝑠   𝑈,𝑠   𝑊,𝑠

Allowed substitution hints:   𝐶(𝑠)   𝑋(𝑠)

Proof of Theorem cdleme31sc

Step	Hyp	Ref	Expression
1		nfcvd 2928	. . 3 ⊢ (𝑅 ∈ 𝐴 → Ⅎ𝑠((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))))
2		oveq1 7426	. . . 4 ⊢ (𝑠 = 𝑅 → (𝑠 ∨ 𝑈) = (𝑅 ∨ 𝑈))
3		oveq2 7427	. . . . . 6 ⊢ (𝑠 = 𝑅 → (𝑃 ∨ 𝑠) = (𝑃 ∨ 𝑅))
4	3	oveq1d 7434	. . . . 5 ⊢ (𝑠 = 𝑅 → ((𝑃 ∨ 𝑠) ∧ 𝑊) = ((𝑃 ∨ 𝑅) ∧ 𝑊))
5	4	oveq2d 7435	. . . 4 ⊢ (𝑠 = 𝑅 → (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)) = (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊)))
6	2, 5	oveq12d 7437	. . 3 ⊢ (𝑠 = 𝑅 → ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))))
7	1, 6	csbiegf 3887	. 2 ⊢ (𝑅 ∈ 𝐴 → ⦋𝑅 / 𝑠⦌((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))))
8		cdleme31sc.c	. . 3 ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)))
9	8	csbeq2i 3862	. 2 ⊢ ⦋𝑅 / 𝑠⦌𝐶 = ⦋𝑅 / 𝑠⦌((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)))
10		cdleme31sc.x	. 2 ⊢ 𝑋 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊)))
11	7, 9, 10	3eqtr4g 2825	1 ⊢ (𝑅 ∈ 𝐴 → ⦋𝑅 / 𝑠⦌𝐶 = 𝑋)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  ⦋csb 3854  (class class class)co 7419

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422

This theorem is used by:  cdleme31snd  41220  cdleme31sdnN  41221  cdlemefr44  41259  cdlemefr45e  41262  cdleme48fv  41333  cdleme46fvaw  41335  cdleme48bw  41336  cdleme46fsvlpq  41339  cdlemeg46fvcl  41340  cdlemeg49le  41345  cdlemeg46fjgN  41355  cdlemeg46rjgN  41356  cdlemeg46fjv  41357  cdleme48d  41369  cdlemeg49lebilem  41373  cdleme50eq  41375  cdleme50f  41376  cdlemg2jlemOLDN  41427  cdlemg2klem  41429