Theorem sbcbiVD 45152

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

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 44851	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ▶   𝐴 ∈ 𝐵   )
2		idn2 44890	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ,   ∀𝑥(𝜑 ↔ 𝜓)   ▶   ∀𝑥(𝜑 ↔ 𝜓)   )
3		spsbc 3754	. . . . 5 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝜑 ↔ 𝜓) → [𝐴 / 𝑥](𝜑 ↔ 𝜓)))
4	1, 2, 3	e12 45000	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ,   ∀𝑥(𝜑 ↔ 𝜓)   ▶   [𝐴 / 𝑥](𝜑 ↔ 𝜓)   )
5		sbcbig 3793	. . . . 5 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)))
6	5	biimpd 229	. . . 4 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)))
7	1, 4, 6	e12 45000	. . 3 ⊢ (   𝐴 ∈ 𝐵   ,   ∀𝑥(𝜑 ↔ 𝜓)   ▶   ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)   )
8	7	in2 44882	. 2 ⊢ (   𝐴 ∈ 𝐵   ▶   (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))   )
9	8	in1 44848	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   ∈ wcel 2114  [wsbc 3741

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3742  df-vd1 44847  df-vd2 44855

This theorem is referenced by: (None)