# Metamath Proof Explorer

## Theorem ssralv2VD

Description: Quantification restricted to a subclass for two quantifiers. ssralv 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 is ssralv2VD without virtual deductions and was automatically derived from ssralv2VD .

 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.)

Ref Expression
Assertion ssralv2VD ${⊢}\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right)\to \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }\right)$

### Proof

Step Hyp Ref Expression
1 ax-5 ${⊢}\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right)$
2 hbra1 ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }$
3 idn1 ${⊢}\left(\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right){\to }\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right)\right)$
4 simpr ${⊢}\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right)\to {C}\subseteq {D}$
5 3 4 e1a ${⊢}\left(\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right){\to }{C}\subseteq {D}\right)$
6 idn3 ${⊢}\left(\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right){,}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }{,}{x}\in {A}{\to }{x}\in {A}\right)$
7 simpl ${⊢}\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right)\to {A}\subseteq {B}$
8 3 7 e1a ${⊢}\left(\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right){\to }{A}\subseteq {B}\right)$
9 idn2 ${⊢}\left(\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right){,}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }{\to }\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
10 ssralv ${⊢}{A}\subseteq {B}\to \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
11 8 9 10 e12 ${⊢}\left(\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right){,}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }{\to }\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
12 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
13 12 biimpi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
14 11 13 e2 ${⊢}\left(\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right){,}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }{\to }\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
15 sp ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left({x}\in {A}\to \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
16 14 15 e2 ${⊢}\left(\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right){,}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }{\to }\left({x}\in {A}\to \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
17 pm2.27 ${⊢}{x}\in {A}\to \left(\left({x}\in {A}\to \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
18 6 16 17 e32 ${⊢}\left(\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right){,}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }{,}{x}\in {A}{\to }\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
19 ssralv ${⊢}{C}\subseteq {D}\to \left(\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
20 5 18 19 e13 ${⊢}\left(\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right){,}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }{,}{x}\in {A}{\to }\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
21 20 in3 ${⊢}\left(\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right){,}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }{\to }\left({x}\in {A}\to \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
22 1 2 21 gen21nv ${⊢}\left(\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right){,}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }{\to }\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
23 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
24 23 biimpri ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }$
25 22 24 e2 ${⊢}\left(\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right){,}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }{\to }\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
26 25 in2 ${⊢}\left(\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right){\to }\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
27 26 in1 ${⊢}\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right)\to \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }\right)$