Step |
Hyp |
Ref |
Expression |
1 |
|
cdleme31se.e |
⊢ 𝐸 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) ) ) |
2 |
|
cdleme31se.y |
⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) ) |
3 |
|
nfcvd |
⊢ ( 𝑅 ∈ 𝐴 → Ⅎ 𝑠 ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) ) ) |
4 |
|
oveq1 |
⊢ ( 𝑠 = 𝑅 → ( 𝑠 ∨ 𝑇 ) = ( 𝑅 ∨ 𝑇 ) ) |
5 |
4
|
oveq1d |
⊢ ( 𝑠 = 𝑅 → ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) = ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) |
6 |
5
|
oveq2d |
⊢ ( 𝑠 = 𝑅 → ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) ) = ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) ) |
7 |
6
|
oveq2d |
⊢ ( 𝑠 = 𝑅 → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) ) ) |
8 |
3 7
|
csbiegf |
⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) ) ) |
9 |
1
|
csbeq2i |
⊢ ⦋ 𝑅 / 𝑠 ⦌ 𝐸 = ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) ) ) |
10 |
8 9 2
|
3eqtr4g |
⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ 𝐸 = 𝑌 ) |