Theorem csbeq2gVD 33173

Description: Virtual deduction proof of csbeq2gOLD 32803. 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. csbeq2gOLD 32803 is csbeq2gVD 33173 without virtual deductions and was automatically derived from csbeq2gVD 33173.

1::	|- (. A e. V ->. A e. V ).
2:1:	|- (. A e. V ->. ( A. x B = C -> [. A / x ]. B = C ) ).
3:1:	|- (. A e. V ->. ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) ).
4:2,3:	|- (. A e. V ->. ( A. x B = C -> [_ A / x ]_ B = [_ A / x ]_ C ) ).
qed:4:	|- ( A e. V -> ( A. x B = C -> [_ A / x ]_ B = [_ A / x ]_ C ) )

(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
csbeq2gVD	|- ( A e. V -> ( A. x B = C -> [_ A / x ]_ B = [_ A / x ]_ C ) )

Proof of Theorem csbeq2gVD

Step	Hyp	Ref	Expression
1		idn1 32832	. . . 4 |- (. A e. V ->. A e. V ).
2		spsbc 3349	. . . 4 |- ( A e. V -> ( A. x B = C -> [. A / x ]. B = C ) )
3	1, 2	e1a 32894	. . 3 |- (. A e. V ->. ( A. x B = C -> [. A / x ]. B = C ) ).
4		sbceqg 3830	. . . 4 |- ( A e. V -> ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) )
5	1, 4	e1a 32894	. . 3 |- (. A e. V ->. ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) ).
6		imbi2 324	. . . 4 |- ( ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) -> ( ( A. x B = C -> [. A / x ]. B = C ) <-> ( A. x B = C -> [_ A / x ]_ B = [_ A / x ]_ C ) ) )
7	6	biimpcd 224	. . 3 |- ( ( A. x B = C -> [. A / x ]. B = C ) -> ( ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) -> ( A. x B = C -> [_ A / x ]_ B = [_ A / x ]_ C ) ) )
8	3, 5, 7	e11 32955	. 2 |- (. A e. V ->. ( A. x B = C -> [_ A / x ]_ B = [_ A / x ]_ C ) ).
9	8	in1 32829	1 |- ( A e. V -> ( A. x B = C -> [_ A / x ]_ B = [_ A / x ]_ C ) )

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1377   = wceq 1379   e. wcel 1767   [.wsbc 3336   [_csb 3440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120  df-sbc 3337  df-csb 3441  df-vd1 32828

This theorem is referenced by: (None)