![]() |
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 3835.
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 43972 is sbcbiVD 44309 without virtual deductions and was automatically
derived from sbcbiVD 44309.
|
Ref | Expression |
---|---|
sbcbiVD | ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idn1 44007 | . . . 4 ⊢ ( 𝐴 ∈ 𝐵 ▶ 𝐴 ∈ 𝐵 ) | |
2 | idn2 44046 | . . . . 5 ⊢ ( 𝐴 ∈ 𝐵 , ∀𝑥(𝜑 ↔ 𝜓) ▶ ∀𝑥(𝜑 ↔ 𝜓) ) | |
3 | spsbc 3788 | . . . . 5 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝜑 ↔ 𝜓) → [𝐴 / 𝑥](𝜑 ↔ 𝜓))) | |
4 | 1, 2, 3 | e12 44157 | . . . 4 ⊢ ( 𝐴 ∈ 𝐵 , ∀𝑥(𝜑 ↔ 𝜓) ▶ [𝐴 / 𝑥](𝜑 ↔ 𝜓) ) |
5 | sbcbig 3829 | . . . . 5 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) | |
6 | 5 | biimpd 228 | . . . 4 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) |
7 | 1, 4, 6 | e12 44157 | . . 3 ⊢ ( 𝐴 ∈ 𝐵 , ∀𝑥(𝜑 ↔ 𝜓) ▶ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) ) |
8 | 7 | in2 44038 | . 2 ⊢ ( 𝐴 ∈ 𝐵 ▶ (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) ) |
9 | 8 | in1 44004 | 1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1532 ∈ wcel 2099 [wsbc 3775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-12 2167 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-tru 1537 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-sbc 3776 df-vd1 44003 df-vd2 44011 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |