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 3743.
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 41773 is sbcbiVD 42110 without virtual deductions and was automatically
derived from sbcbiVD 42110.
|
Ref | Expression |
---|---|
sbcbiVD | ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idn1 41808 | . . . 4 ⊢ ( 𝐴 ∈ 𝐵 ▶ 𝐴 ∈ 𝐵 ) | |
2 | idn2 41847 | . . . . 5 ⊢ ( 𝐴 ∈ 𝐵 , ∀𝑥(𝜑 ↔ 𝜓) ▶ ∀𝑥(𝜑 ↔ 𝜓) ) | |
3 | spsbc 3696 | . . . . 5 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝜑 ↔ 𝜓) → [𝐴 / 𝑥](𝜑 ↔ 𝜓))) | |
4 | 1, 2, 3 | e12 41958 | . . . 4 ⊢ ( 𝐴 ∈ 𝐵 , ∀𝑥(𝜑 ↔ 𝜓) ▶ [𝐴 / 𝑥](𝜑 ↔ 𝜓) ) |
5 | sbcbig 3737 | . . . . 5 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) | |
6 | 5 | biimpd 232 | . . . 4 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) |
7 | 1, 4, 6 | e12 41958 | . . 3 ⊢ ( 𝐴 ∈ 𝐵 , ∀𝑥(𝜑 ↔ 𝜓) ▶ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) ) |
8 | 7 | in2 41839 | . 2 ⊢ ( 𝐴 ∈ 𝐵 ▶ (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) ) |
9 | 8 | in1 41805 | 1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∀wal 1541 ∈ wcel 2112 [wsbc 3683 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-12 2177 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-nf 1792 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-sbc 3684 df-vd1 41804 df-vd2 41812 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |