Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sbcssgVD Structured version   Unicode version

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.
StepHypRef 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 ) )
31, 2e1a 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 ) )
51, 4e1a 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 ) ) ) )
73, 5, 6e11 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
) ) )
91, 8e1a 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 ) ) ) )
1110biimprcd 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 ) ) ) )
127, 9, 11e11 36709 . . . . . . 7  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( y  e.  C  ->  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  ->  y  e. 
[_ A  /  x ]_ D ) ) ).
1312gen11 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 ) ) )
1513, 14e1a 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 ) ) )
171, 16e1a 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 ) ) ) )
1918biimprcd 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 ) ) ) )
2015, 17, 19e11 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 ) )
2221ax-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 ) ) ) )
241, 22, 23e10 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 ) ) ) )
2625biimprcd 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 ) ) ) )
2720, 24, 26e11 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 ) )
3029ex 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 ) ) )
3127, 28, 30e10 36715 . 2  |-  (. A  e.  B  ->.  ( [. A  /  x ]. C  C_  D 
<-> 
[_ A  /  x ]_ C  C_  [_ A  /  x ]_ D ) ).
3231in1 36583 1  |-  ( A  e.  B  ->  ( [. A  /  x ]. C  C_  D  <->  [_ A  /  x ]_ C  C_  [_ A  /  x ]_ D ) )
Colors of variables: wff setvar class
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)
  Copyright terms: Public domain W3C validator