![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > csbeq2gVD | Structured version Visualization version GIF version |
Description: Virtual deduction proof of csbeq2 3898.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
csbeq2 3898 is csbeq2gVD 44115 without virtual deductions and was
automatically derived from csbeq2gVD 44115.
|
Ref | Expression |
---|---|
csbeq2gVD | ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idn1 43797 | . . . 4 ⊢ ( 𝐴 ∈ 𝑉 ▶ 𝐴 ∈ 𝑉 ) | |
2 | spsbc 3790 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 𝐵 = 𝐶 → [𝐴 / 𝑥]𝐵 = 𝐶)) | |
3 | 1, 2 | e1a 43850 | . . 3 ⊢ ( 𝐴 ∈ 𝑉 ▶ (∀𝑥 𝐵 = 𝐶 → [𝐴 / 𝑥]𝐵 = 𝐶) ) |
4 | sbceqg 4409 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) | |
5 | 1, 4 | e1a 43850 | . . 3 ⊢ ( 𝐴 ∈ 𝑉 ▶ ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) ) |
6 | imbi2 348 | . . . 4 ⊢ (([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) → ((∀𝑥 𝐵 = 𝐶 → [𝐴 / 𝑥]𝐵 = 𝐶) ↔ (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))) | |
7 | 6 | biimpcd 248 | . . 3 ⊢ ((∀𝑥 𝐵 = 𝐶 → [𝐴 / 𝑥]𝐵 = 𝐶) → (([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) → (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))) |
8 | 3, 5, 7 | e11 43911 | . 2 ⊢ ( 𝐴 ∈ 𝑉 ▶ (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) ) |
9 | 8 | in1 43794 | 1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1538 = wceq 1540 ∈ wcel 2105 [wsbc 3777 ⦋csb 3893 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-tru 1543 df-ex 1781 df-nf 1785 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-sbc 3778 df-csb 3894 df-vd1 43793 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |