Theorem ssralv2 38737

Description: Quantification restricted to a subclass for two quantifiers. ssralv 3666 for two quantifiers. The proof of ssralv2 38737 was automatically generated by minimizing the automatically translated proof of ssralv2VD 39102. The automatic translation is by the tools program translate_without_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

Step	Hyp	Ref	Expression
1		nfv 1843	. 2 |- F/ x ( A C_ B /\ C C_ D )
2		nfra1 2941	. 2 |- F/ x A. x e. B A. y e. D ph
3		ssralv 3666	. . . . . 6 |- ( A C_ B -> ( A. x e. B A. y e. D ph -> A. x e. A A. y e. D ph ) )
4	3	adantr 481	. . . . 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 2917	. . . . 5 |- ( A. x e. A A. y e. D ph <-> A. x ( x e. A -> A. y e. D ph ) )
6	4, 5	syl6ib 241	. . . 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 2053	. . . 4 |- ( A. x ( x e. A -> A. y e. D ph ) -> ( x e. A -> A. y e. D ph ) )
8	6, 7	syl6 35	. . 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 3666	. . . 4 |- ( C C_ D -> ( A. y e. D ph -> A. y e. C ph ) )
10	9	adantl 482	. . 3 |- ( ( A C_ B /\ C C_ D ) -> ( A. y e. D ph -> A. y e. C ph ) )
11	8, 10	syl6d 75	. 2 |- ( ( A C_ B /\ C C_ D ) -> ( A. x e. B A. y e. D ph -> ( x e. A -> A. y e. C ph ) ) )
12	1, 2, 11	ralrimd 2959	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 ) )

Syntax hints:   -> wi 4   /\ wa 384   A.wal 1481   e. wcel 1990   A.wral 2912   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-in 3581  df-ss 3588

This theorem is referenced by:  ordelordALT  38747  ordelordALTVD  39103