![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > cdleme31sc | Structured version Visualization version GIF version |
Description: Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.) |
Ref | Expression |
---|---|
cdleme31sc.c | ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) |
cdleme31sc.x | ⊢ 𝑋 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) |
Ref | Expression |
---|---|
cdleme31sc | ⊢ (𝑅 ∈ 𝐴 → ⦋𝑅 / 𝑠⦌𝐶 = 𝑋) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcvd 2903 | . . 3 ⊢ (𝑅 ∈ 𝐴 → Ⅎ𝑠((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊)))) | |
2 | oveq1 7437 | . . . 4 ⊢ (𝑠 = 𝑅 → (𝑠 ∨ 𝑈) = (𝑅 ∨ 𝑈)) | |
3 | oveq2 7438 | . . . . . 6 ⊢ (𝑠 = 𝑅 → (𝑃 ∨ 𝑠) = (𝑃 ∨ 𝑅)) | |
4 | 3 | oveq1d 7445 | . . . . 5 ⊢ (𝑠 = 𝑅 → ((𝑃 ∨ 𝑠) ∧ 𝑊) = ((𝑃 ∨ 𝑅) ∧ 𝑊)) |
5 | 4 | oveq2d 7446 | . . . 4 ⊢ (𝑠 = 𝑅 → (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)) = (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) |
6 | 2, 5 | oveq12d 7448 | . . 3 ⊢ (𝑠 = 𝑅 → ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊)))) |
7 | 1, 6 | csbiegf 3941 | . 2 ⊢ (𝑅 ∈ 𝐴 → ⦋𝑅 / 𝑠⦌((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊)))) |
8 | cdleme31sc.c | . . 3 ⊢ 𝐶 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) | |
9 | 8 | csbeq2i 3915 | . 2 ⊢ ⦋𝑅 / 𝑠⦌𝐶 = ⦋𝑅 / 𝑠⦌((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) |
10 | cdleme31sc.x | . 2 ⊢ 𝑋 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) | |
11 | 7, 9, 10 | 3eqtr4g 2799 | 1 ⊢ (𝑅 ∈ 𝐴 → ⦋𝑅 / 𝑠⦌𝐶 = 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1536 ∈ wcel 2105 ⦋csb 3907 (class class class)co 7430 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-iota 6515 df-fv 6570 df-ov 7433 |
This theorem is referenced by: cdleme31snd 40368 cdleme31sdnN 40369 cdlemefr44 40407 cdlemefr45e 40410 cdleme48fv 40481 cdleme46fvaw 40483 cdleme48bw 40484 cdleme46fsvlpq 40487 cdlemeg46fvcl 40488 cdlemeg49le 40493 cdlemeg46fjgN 40503 cdlemeg46rjgN 40504 cdlemeg46fjv 40505 cdleme48d 40517 cdlemeg49lebilem 40521 cdleme50eq 40523 cdleme50f 40524 cdlemg2jlemOLDN 40575 cdlemg2klem 40577 |
Copyright terms: Public domain | W3C validator |