![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > sbcbiVD | Structured version Visualization version GIF version |
Description: Implication form of sbcbii 3830.
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 43814 is sbcbiVD 44151 without virtual deductions and was automatically
derived from sbcbiVD 44151.
|
Ref | Expression |
---|---|
sbcbiVD | ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idn1 43849 | . . . 4 ⊢ ( 𝐴 ∈ 𝐵 ▶ 𝐴 ∈ 𝐵 ) | |
2 | idn2 43888 | . . . . 5 ⊢ ( 𝐴 ∈ 𝐵 , ∀𝑥(𝜑 ↔ 𝜓) ▶ ∀𝑥(𝜑 ↔ 𝜓) ) | |
3 | spsbc 3783 | . . . . 5 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝜑 ↔ 𝜓) → [𝐴 / 𝑥](𝜑 ↔ 𝜓))) | |
4 | 1, 2, 3 | e12 43999 | . . . 4 ⊢ ( 𝐴 ∈ 𝐵 , ∀𝑥(𝜑 ↔ 𝜓) ▶ [𝐴 / 𝑥](𝜑 ↔ 𝜓) ) |
5 | sbcbig 3824 | . . . . 5 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) | |
6 | 5 | biimpd 228 | . . . 4 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) |
7 | 1, 4, 6 | e12 43999 | . . 3 ⊢ ( 𝐴 ∈ 𝐵 , ∀𝑥(𝜑 ↔ 𝜓) ▶ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) ) |
8 | 7 | in2 43880 | . 2 ⊢ ( 𝐴 ∈ 𝐵 ▶ (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) ) |
9 | 8 | in1 43846 | 1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1531 ∈ wcel 2098 [wsbc 3770 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-12 2163 ax-ext 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-tru 1536 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-sbc 3771 df-vd1 43845 df-vd2 43853 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |