|   | 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 3903.
     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 3903 is csbeq2gVD 44917 without virtual deductions and was
     automatically derived from csbeq2gVD 44917. 
 | 
| Ref | Expression | 
|---|---|
| csbeq2gVD | ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | idn1 44599 | . . . 4 ⊢ ( 𝐴 ∈ 𝑉 ▶ 𝐴 ∈ 𝑉 ) | |
| 2 | spsbc 3800 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 𝐵 = 𝐶 → [𝐴 / 𝑥]𝐵 = 𝐶)) | |
| 3 | 1, 2 | e1a 44652 | . . 3 ⊢ ( 𝐴 ∈ 𝑉 ▶ (∀𝑥 𝐵 = 𝐶 → [𝐴 / 𝑥]𝐵 = 𝐶) ) | 
| 4 | sbceqg 4411 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) | |
| 5 | 1, 4 | e1a 44652 | . . 3 ⊢ ( 𝐴 ∈ 𝑉 ▶ ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) ) | 
| 6 | imbi2 348 | . . . 4 ⊢ (([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) → ((∀𝑥 𝐵 = 𝐶 → [𝐴 / 𝑥]𝐵 = 𝐶) ↔ (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))) | |
| 7 | 6 | biimpcd 249 | . . 3 ⊢ ((∀𝑥 𝐵 = 𝐶 → [𝐴 / 𝑥]𝐵 = 𝐶) → (([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) → (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))) | 
| 8 | 3, 5, 7 | e11 44713 | . 2 ⊢ ( 𝐴 ∈ 𝑉 ▶ (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) ) | 
| 9 | 8 | in1 44596 | 1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1537 = wceq 1539 ∈ wcel 2107 [wsbc 3787 ⦋csb 3898 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1542 df-ex 1779 df-nf 1783 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-sbc 3788 df-csb 3899 df-vd1 44595 | 
| This theorem is referenced by: (None) | 
| Copyright terms: Public domain | W3C validator |