Theorem sbcbiVD 41230

Description: Implication form of sbcbii 3829. 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 40893 is sbcbiVD 41230 without virtual deductions and was automatically derived from sbcbiVD 41230.

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

Step	Hyp	Ref	Expression
1		idn1 40928	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ▶   𝐴 ∈ 𝐵   )
2		idn2 40967	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ,   ∀𝑥(𝜑 ↔ 𝜓)   ▶   ∀𝑥(𝜑 ↔ 𝜓)   )
3		spsbc 3785	. . . . 5 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝜑 ↔ 𝜓) → [𝐴 / 𝑥](𝜑 ↔ 𝜓)))
4	1, 2, 3	e12 41078	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ,   ∀𝑥(𝜑 ↔ 𝜓)   ▶   [𝐴 / 𝑥](𝜑 ↔ 𝜓)   )
5		sbcbig 3823	. . . . 5 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)))
6	5	biimpd 231	. . . 4 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)))
7	1, 4, 6	e12 41078	. . 3 ⊢ (   𝐴 ∈ 𝐵   ,   ∀𝑥(𝜑 ↔ 𝜓)   ▶   ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)   )
8	7	in2 40959	. 2 ⊢ (   𝐴 ∈ 𝐵   ▶   (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))   )
9	8	in1 40925	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535   ∈ wcel 2114  [wsbc 3772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-sbc 3773  df-vd1 40924  df-vd2 40932

This theorem is referenced by: (None)