Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sbcbiVD Structured version   Visualization version   GIF version

Theorem sbcbiVD 41569
Description: Implication form of sbcbii 3779. 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. sbcbi 41232 is sbcbiVD 41569 without virtual deductions and was automatically derived from sbcbiVD 41569.
 1:: ⊢ (   𝐴 ∈ 𝐵   ▶   𝐴 ∈ 𝐵   ) 2:: ⊢ (   𝐴 ∈ 𝐵   ,   ∀𝑥(𝜑 ↔ 𝜓)    ▶   ∀𝑥(𝜑 ↔ 𝜓)   ) 3:1,2: ⊢ (   𝐴 ∈ 𝐵   ,   ∀𝑥(𝜑 ↔ 𝜓)    ▶   [𝐴 / 𝑥](𝜑 ↔ 𝜓)   ) 4:1,3: ⊢ (   𝐴 ∈ 𝐵   ,   ∀𝑥(𝜑 ↔ 𝜓)    ▶   ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)   ) 5:4: ⊢ (   𝐴 ∈ 𝐵   ▶   (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))   ) qed:5: ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)))
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
sbcbiVD (𝐴𝐵 → (∀𝑥(𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))

Proof of Theorem sbcbiVD
StepHypRef Expression
1 idn1 41267 . . . 4 (   𝐴𝐵   ▶   𝐴𝐵   )
2 idn2 41306 . . . . 5 (   𝐴𝐵   ,   𝑥(𝜑𝜓)   ▶   𝑥(𝜑𝜓)   )
3 spsbc 3736 . . . . 5 (𝐴𝐵 → (∀𝑥(𝜑𝜓) → [𝐴 / 𝑥](𝜑𝜓)))
41, 2, 3e12 41417 . . . 4 (   𝐴𝐵   ,   𝑥(𝜑𝜓)   ▶   [𝐴 / 𝑥](𝜑𝜓)   )
5 sbcbig 3773 . . . . 5 (𝐴𝐵 → ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
65biimpd 232 . . . 4 (𝐴𝐵 → ([𝐴 / 𝑥](𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
71, 4, 6e12 41417 . . 3 (   𝐴𝐵   ,   𝑥(𝜑𝜓)   ▶   ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)   )
87in2 41298 . 2 (   𝐴𝐵   ▶   (∀𝑥(𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))   )
98in1 41264 1 (𝐴𝐵 → (∀𝑥(𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   ∈ wcel 2112  [wsbc 3723 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-12 2176  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-sbc 3724  df-vd1 41263  df-vd2 41271 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator