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

Theorem ssralv2 28616
Description: Quantification restricted to a subclass for two quantifiers. ssralv 3408 for two quantifiers. The proof of ssralv2 28616 was automatically generated by minimizing the automatically translated proof of ssralv2VD 28979. The automatic translation is by the tools program translatewithout_overwriting.cmd (Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ssralv2  |-  ( ( 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 ssralv2
StepHypRef Expression
1 nfv 1630 . 2  |-  F/ x
( A  C_  B  /\  C  C_  D )
2 nfra1 2757 . 2  |-  F/ x A. x  e.  B  A. y  e.  D  ph
3 ssralv 3408 . . . . . 6  |-  ( A 
C_  B  ->  ( A. x  e.  B  A. y  e.  D  ph 
->  A. x  e.  A  A. y  e.  D  ph ) )
43adantr 453 . . . . 5  |-  ( ( 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 df-ral 2711 . . . . 5  |-  ( A. x  e.  A  A. y  e.  D  ph  <->  A. x
( x  e.  A  ->  A. y  e.  D  ph ) )
64, 5syl6ib 219 . . . 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 ) ) )
7 sp 1764 . . . 4  |-  ( A. x ( x  e.  A  ->  A. y  e.  D  ph )  -> 
( x  e.  A  ->  A. y  e.  D  ph ) )
86, 7syl6 32 . . 3  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A. x  e.  B  A. y  e.  D  ph  ->  (
x  e.  A  ->  A. y  e.  D  ph ) ) )
9 ssralv 3408 . . . 4  |-  ( C 
C_  D  ->  ( A. y  e.  D  ph 
->  A. y  e.  C  ph ) )
109adantl 454 . . 3  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A. y  e.  D  ph  ->  A. y  e.  C  ph ) )
118, 10syl6d 67 . 2  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A. x  e.  B  A. y  e.  D  ph  ->  (
x  e.  A  ->  A. y  e.  C  ph ) ) )
121, 2, 11ralrimd 2795 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 set class
Syntax hints:    -> wi 4    /\ wa 360   A.wal 1550    e. wcel 1726   A.wral 2706    C_ wss 3321
This theorem is referenced by:  ordelordALT  28623  ordelordALTVD  28980
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-ral 2711  df-in 3328  df-ss 3335
  Copyright terms: Public domain W3C validator