# Metamath Proof Explorer

## Theorem ssralv2

Description: Quantification restricted to a subclass for two quantifiers. ssralv for two quantifiers. The proof of ssralv2 was automatically generated by minimizing the automatically translated proof of ssralv2VD . 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.)

Ref Expression
Assertion ssralv2 ${⊢}\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 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right)$
2 nfra1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }$
3 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)$
4 3 adantr ${⊢}\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 {D}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
5 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)$
6 4 5 syl6ib ${⊢}\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}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
7 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)$
8 6 7 syl6 ${⊢}\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 \left({x}\in {A}\to \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
9 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)$
10 9 adantl ${⊢}\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right)\to \left(\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
11 8 10 syl6d ${⊢}\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 \left({x}\in {A}\to \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
12 1 2 11 ralrimd ${⊢}\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)$