Theorem sbcssgVD 36924

Description: Virtual deduction proof of sbcssg 3905. 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. sbcssg 3905 is sbcssgVD 36924 without virtual deductions and was automatically derived from sbcssgVD 36924.

1::	|- (. A e. B ->. A e. B ).
2:1:	|- (. A e. B ->. ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) ).
3:1:	|- (. A e. B ->. ( [. A / x ]. y e. D <-> y e. [_ A / x ]_ D ) ).
4:2,3:	|- (. A e. B ->. ( ( [. A / x ]. y e. C -> [. A / x ]. y e. D ) <-> ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
5:1:	|- (. A e. B ->. ( [. A / x ]. ( y e. C -> y e. D ) <-> ( [. A / x ]. y e. C -> [. A / x ]. y e. D ) ) ).
6:4,5:	|- (. A e. B ->. ( [. A / x ]. ( y e. C -> y e. D ) <-> ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
7:6:	|- (. A e. B ->. A. y ( [. A / x ]. ( y e. C -> y e. D ) <-> ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
8:7:	|- (. A e. B ->. ( A. y [. A / x ]. ( y e. C -> y e. D ) <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
9:1:	|- (. A e. B ->. ( [. A / x ]. A. y ( y e. C -> y e. D ) <-> A. y [. A / x ]. ( y e. C -> y e. D ) ) ).
10:8,9:	|- (. A e. B ->. ( [. A / x ]. A. y ( y e. C -> y e. D ) <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
11::	|- ( C C_ D <-> A. y ( y e. C -> y e. D ) )
110:11:	|- A. x ( C C_ D <-> A. y ( y e. C -> y e. D ) )
12:1,110:	|- (. A e. B ->. ( [. A / x ]. C C_ D <-> [. A / x ]. A. y ( y e. C -> y e. D ) ) ).
13:10,12:	|- (. A e. B ->. ( [. A / x ]. C C_ D <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
14::	|- ( [_ A / x ]_ C C_ [_ A / x ]_ D <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) )
15:13,14:	|- (. A e. B ->. ( [. A / x ]. C C_ D <-> [_ A / x ]_ C C_ [_ A / x ]_ D ) ).
qed:15:	|- ( A e. B -> ( [. A / x ]. C C_ D <-> [_ A / x ]_ C C_ [_ A / x ]_ D ) )

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

Assertion

Ref	Expression
sbcssgVD	|- ( A e. B -> ( [. A / x ]. C C_ D <-> [_ A / x ]_ C C_ [_ A / x ]_ D ) )

Proof of Theorem sbcssgVD

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		idn1 36586	. . . . . . . . . 10 |- (. A e. B ->. A e. B ).
2		sbcel2gOLD 36547	. . . . . . . . . 10 |- ( A e. B -> ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) )
3	1, 2	e1a 36648	. . . . . . . . 9 |- (. A e. B ->. ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) ).
4		sbcel2gOLD 36547	. . . . . . . . . 10 |- ( A e. B -> ( [. A / x ]. y e. D <-> y e. [_ A / x ]_ D ) )
5	1, 4	e1a 36648	. . . . . . . . 9 |- (. A e. B ->. ( [. A / x ]. y e. D <-> y e. [_ A / x ]_ D ) ).
6		imbi12 323	. . . . . . . . 9 |- ( ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) -> ( ( [. A / x ]. y e. D <-> y e. [_ A / x ]_ D ) -> ( ( [. A / x ]. y e. C -> [. A / x ]. y e. D ) <-> ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ) )
7	3, 5, 6	e11 36709	. . . . . . . 8 |- (. A e. B ->. ( ( [. A / x ]. y e. C -> [. A / x ]. y e. D ) <-> ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
8		sbcimg 3338	. . . . . . . . 9 |- ( A e. B -> ( [. A / x ]. ( y e. C -> y e. D ) <-> ( [. A / x ]. y e. C -> [. A / x ]. y e. D ) ) )
9	1, 8	e1a 36648	. . . . . . . 8 |- (. A e. B ->. ( [. A / x ]. ( y e. C -> y e. D ) <-> ( [. A / x ]. y e. C -> [. A / x ]. y e. D ) ) ).
10		bibi1 328	. . . . . . . . 9 |- ( ( [. A / x ]. ( y e. C -> y e. D ) <-> ( [. A / x ]. y e. C -> [. A / x ]. y e. D ) ) -> ( ( [. A / x ]. ( y e. C -> y e. D ) <-> ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) <-> ( ( [. A / x ]. y e. C -> [. A / x ]. y e. D ) <-> ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ) )
11	10	biimprcd 228	. . . . . . . 8 |- ( ( ( [. A / x ]. y e. C -> [. A / x ]. y e. D ) <-> ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) -> ( ( [. A / x ]. ( y e. C -> y e. D ) <-> ( [. A / x ]. y e. C -> [. A / x ]. y e. D ) ) -> ( [. A / x ]. ( y e. C -> y e. D ) <-> ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ) )
12	7, 9, 11	e11 36709	. . . . . . 7 |- (. A e. B ->. ( [. A / x ]. ( y e. C -> y e. D ) <-> ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
13	12	gen11 36637	. . . . . 6 |- (. A e. B ->. A. y ( [. A / x ]. ( y e. C -> y e. D ) <-> ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
14		albi 1686	. . . . . 6 |- ( A. y ( [. A / x ]. ( y e. C -> y e. D ) <-> ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) -> ( A. y [. A / x ]. ( y e. C -> y e. D ) <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) )
15	13, 14	e1a 36648	. . . . 5 |- (. A e. B ->. ( A. y [. A / x ]. ( y e. C -> y e. D ) <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
16		sbcalgOLD 36544	. . . . . 6 |- ( A e. B -> ( [. A / x ]. A. y ( y e. C -> y e. D ) <-> A. y [. A / x ]. ( y e. C -> y e. D ) ) )
17	1, 16	e1a 36648	. . . . 5 |- (. A e. B ->. ( [. A / x ]. A. y ( y e. C -> y e. D ) <-> A. y [. A / x ]. ( y e. C -> y e. D ) ) ).
18		bibi1 328	. . . . . 6 |- ( ( [. A / x ]. A. y ( y e. C -> y e. D ) <-> A. y [. A / x ]. ( y e. C -> y e. D ) ) -> ( ( [. A / x ]. A. y ( y e. C -> y e. D ) <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) <-> ( A. y [. A / x ]. ( y e. C -> y e. D ) <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ) )
19	18	biimprcd 228	. . . . 5 |- ( ( A. y [. A / x ]. ( y e. C -> y e. D ) <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) -> ( ( [. A / x ]. A. y ( y e. C -> y e. D ) <-> A. y [. A / x ]. ( y e. C -> y e. D ) ) -> ( [. A / x ]. A. y ( y e. C -> y e. D ) <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ) )
20	15, 17, 19	e11 36709	. . . 4 |- (. A e. B ->. ( [. A / x ]. A. y ( y e. C -> y e. D ) <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
21		dfss2 3450	. . . . . 6 |- ( C C_ D <-> A. y ( y e. C -> y e. D ) )
22	21	ax-gen 1665	. . . . 5 |- A. x ( C C_ D <-> A. y ( y e. C -> y e. D ) )
23		sbcbi 36541	. . . . 5 |- ( A e. B -> ( A. x ( C C_ D <-> A. y ( y e. C -> y e. D ) ) -> ( [. A / x ]. C C_ D <-> [. A / x ]. A. y ( y e. C -> y e. D ) ) ) )
24	1, 22, 23	e10 36715	. . . 4 |- (. A e. B ->. ( [. A / x ]. C C_ D <-> [. A / x ]. A. y ( y e. C -> y e. D ) ) ).
25		bibi1 328	. . . . 5 |- ( ( [. A / x ]. C C_ D <-> [. A / x ]. A. y ( y e. C -> y e. D ) ) -> ( ( [. A / x ]. C C_ D <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) <-> ( [. A / x ]. A. y ( y e. C -> y e. D ) <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ) )
26	25	biimprcd 228	. . . 4 |- ( ( [. A / x ]. A. y ( y e. C -> y e. D ) <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) -> ( ( [. A / x ]. C C_ D <-> [. A / x ]. A. y ( y e. C -> y e. D ) ) -> ( [. A / x ]. C C_ D <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ) )
27	20, 24, 26	e11 36709	. . 3 |- (. A e. B ->. ( [. A / x ]. C C_ D <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ).
28		dfss2 3450	. . 3 |- ( [_ A / x ]_ C C_ [_ A / x ]_ D <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) )
29		biantr 939	. . . 4 |- ( ( ( [. A / x ]. C C_ D <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) /\ ( [_ A / x ]_ C C_ [_ A / x ]_ D <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) ) -> ( [. A / x ]. C C_ D <-> [_ A / x ]_ C C_ [_ A / x ]_ D ) )
30	29	ex 435	. . 3 |- ( ( [. A / x ]. C C_ D <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) -> ( ( [_ A / x ]_ C C_ [_ A / x ]_ D <-> A. y ( y e. [_ A / x ]_ C -> y e. [_ A / x ]_ D ) ) -> ( [. A / x ]. C C_ D <-> [_ A / x ]_ C C_ [_ A / x ]_ D ) ) )
31	27, 28, 30	e10 36715	. 2 |- (. A e. B ->. ( [. A / x ]. C C_ D <-> [_ A / x ]_ C C_ [_ A / x ]_ D ) ).
32	31	in1 36583	1 |- ( A e. B -> ( [. A / x ]. C C_ D <-> [_ A / x ]_ C C_ [_ A / x ]_ D ) )

Syntax hints:   -> wi 4   <-> wb 187   A.wal 1435   e. wcel 1867   [.wsbc 3296   [_csb 3392   C_ wss 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-sbc 3297  df-csb 3393  df-in 3440  df-ss 3447  df-vd1 36582

This theorem is referenced by: (None)