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

Theorem ssralv2VD 33399
Description: Quantification restricted to a subclass for two quantifiers. ssralv 3549 for two quantifiers. 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. ssralv2 33034 is ssralv2VD 33399 without virtual deductions and was automatically derived from ssralv2VD 33399.
1::  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  ( A  C_  B  /\  C  C_  D ) ).
2::  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  A. x  e.  B A. y  e.  D ph ).
3:1:  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  A  C_  B ).
4:3,2:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  A. x  e.  A A. y  e.  D ph ).
5:4:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  A. x ( x  e.  A  ->  A. y  e.  D ph ) ).
6:5:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  ( x  e.  A  ->  A. y  e.  D ph ) ).
7::  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph ,  x  e.  A  ->.  x  e.  A ).
8:7,6:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph ,  x  e.  A  ->.  A. y  e.  D ph ).
9:1:  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  C  C_  D ).
10:9,8:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph ,  x  e.  A  ->.  A. y  e.  C ph ).
11:10:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  ( x  e.  A  ->  A. y  e.  C ph ) ).
12::  |-  ( ( A  C_  B  /\  C  C_  D )  ->  A. x ( A  C_  B  /\  C  C_  D ) )
13::  |-  ( A. x  e.  B A. y  e.  D ph  ->  A. x A. x  e.  B A. y  e.  D ph )
14:12,13,11:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  A. x ( x  e.  A  ->  A. y  e.  C ph ) ).
15:14:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  A. x  e.  A A. y  e.  C ph ).
16:15:  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  ( A. x  e.  B A. y  e.  D ph  ->  A. x  e.  A A. y  e.  C ph ) ).
qed:16:  |-  ( ( A  C_  B  /\  C  C_  D )  ->  ( A. x  e.  B A. y  e.  D ph  ->  A. x  e.  A A. y  e.  C ph ) )
(Contributed by Alan Sare, 10-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ssralv2VD  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A. x  e.  B  A. y  e.  D  ph  ->  A. x  e.  A  A. y  e.  C  ph ) )
Distinct variable groups:    x, A    x, B    x, C    y, C    x, D    y, D
Allowed substitution hints:    ph( x, y)    A( y)    B( y)

Proof of Theorem ssralv2VD
StepHypRef Expression
1 ax-5 1691 . . . . 5  |-  ( ( A  C_  B  /\  C  C_  D )  ->  A. x ( A  C_  B  /\  C  C_  D
) )
2 hbra1 2825 . . . . 5  |-  ( A. x  e.  B  A. y  e.  D  ph  ->  A. x A. x  e.  B  A. y  e.  D  ph )
3 idn1 33084 . . . . . . . 8  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  ( A  C_  B  /\  C  C_  D ) ).
4 simpr 461 . . . . . . . 8  |-  ( ( A  C_  B  /\  C  C_  D )  ->  C  C_  D )
53, 4e1a 33146 . . . . . . 7  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  C  C_  D ).
6 idn3 33134 . . . . . . . 8  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph ,. x  e.  A  ->.  x  e.  A ).
7 simpl 457 . . . . . . . . . . . 12  |-  ( ( A  C_  B  /\  C  C_  D )  ->  A  C_  B )
83, 7e1a 33146 . . . . . . . . . . 11  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  A  C_  B ).
9 idn2 33132 . . . . . . . . . . 11  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph  ->.  A. x  e.  B  A. y  e.  D  ph ).
10 ssralv 3549 . . . . . . . . . . 11  |-  ( A 
C_  B  ->  ( A. x  e.  B  A. y  e.  D  ph 
->  A. x  e.  A  A. y  e.  D  ph ) )
118, 9, 10e12 33254 . . . . . . . . . 10  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph  ->.  A. x  e.  A  A. y  e.  D  ph ).
12 df-ral 2798 . . . . . . . . . . 11  |-  ( A. x  e.  A  A. y  e.  D  ph  <->  A. x
( x  e.  A  ->  A. y  e.  D  ph ) )
1312biimpi 194 . . . . . . . . . 10  |-  ( A. x  e.  A  A. y  e.  D  ph  ->  A. x ( x  e.  A  ->  A. y  e.  D  ph ) )
1411, 13e2 33150 . . . . . . . . 9  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph  ->.  A. x
( x  e.  A  ->  A. y  e.  D  ph ) ).
15 sp 1845 . . . . . . . . 9  |-  ( A. x ( x  e.  A  ->  A. y  e.  D  ph )  -> 
( x  e.  A  ->  A. y  e.  D  ph ) )
1614, 15e2 33150 . . . . . . . 8  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph  ->.  ( x  e.  A  ->  A. y  e.  D  ph ) ).
17 pm2.27 39 . . . . . . . 8  |-  ( x  e.  A  ->  (
( x  e.  A  ->  A. y  e.  D  ph )  ->  A. y  e.  D  ph ) )
186, 16, 17e32 33288 . . . . . . 7  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph ,. x  e.  A  ->.  A. y  e.  D  ph ).
19 ssralv 3549 . . . . . . 7  |-  ( C 
C_  D  ->  ( A. y  e.  D  ph 
->  A. y  e.  C  ph ) )
205, 18, 19e13 33278 . . . . . 6  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph ,. x  e.  A  ->.  A. y  e.  C  ph ).
2120in3 33128 . . . . 5  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph  ->.  ( x  e.  A  ->  A. y  e.  C  ph ) ).
221, 2, 21gen21nv 33139 . . . 4  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph  ->.  A. x
( x  e.  A  ->  A. y  e.  C  ph ) ).
23 df-ral 2798 . . . . 5  |-  ( A. x  e.  A  A. y  e.  C  ph  <->  A. x
( x  e.  A  ->  A. y  e.  C  ph ) )
2423biimpri 206 . . . 4  |-  ( A. x ( x  e.  A  ->  A. y  e.  C  ph )  ->  A. x  e.  A  A. y  e.  C  ph )
2522, 24e2 33150 . . 3  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph  ->.  A. x  e.  A  A. y  e.  C  ph ).
2625in2 33124 . 2  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  ( A. x  e.  B  A. y  e.  D  ph  ->  A. x  e.  A  A. y  e.  C  ph ) ).
2726in1 33081 1  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A. x  e.  B  A. y  e.  D  ph  ->  A. x  e.  A  A. y  e.  C  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wal 1381    e. wcel 1804   A.wral 2793    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-ral 2798  df-in 3468  df-ss 3475  df-vd1 33080  df-vd2 33088  df-vd3 33100
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator