# Metamath Proof Explorer

## Theorem raliunxp

Description: Write a double restricted quantification as one universal quantifier. In this version of ralxp , B ( y ) is not assumed to be constant. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypothesis ralxp.1 ${⊢}{x}=⟨{y},{z}⟩\to \left({\phi }↔{\psi }\right)$
Assertion raliunxp ${⊢}\forall {x}\in \bigcup _{{y}\in {A}}\left(\left\{{y}\right\}×{B}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

Step Hyp Ref Expression
1 ralxp.1 ${⊢}{x}=⟨{y},{z}⟩\to \left({\phi }↔{\psi }\right)$
2 eliunxp ${⊢}{x}\in \bigcup _{{y}\in {A}}\left(\left\{{y}\right\}×{B}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\wedge \left({y}\in {A}\wedge {z}\in {B}\right)\right)$
3 2 imbi1i ${⊢}\left({x}\in \bigcup _{{y}\in {A}}\left(\left\{{y}\right\}×{B}\right)\to {\phi }\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\wedge \left({y}\in {A}\wedge {z}\in {B}\right)\right)\to {\phi }\right)$
4 19.23vv ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{y},{z}⟩\wedge \left({y}\in {A}\wedge {z}\in {B}\right)\right)\to {\phi }\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\wedge \left({y}\in {A}\wedge {z}\in {B}\right)\right)\to {\phi }\right)$
5 3 4 bitr4i ${⊢}\left({x}\in \bigcup _{{y}\in {A}}\left(\left\{{y}\right\}×{B}\right)\to {\phi }\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{y},{z}⟩\wedge \left({y}\in {A}\wedge {z}\in {B}\right)\right)\to {\phi }\right)$
6 5 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \bigcup _{{y}\in {A}}\left(\left\{{y}\right\}×{B}\right)\to {\phi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{y},{z}⟩\wedge \left({y}\in {A}\wedge {z}\in {B}\right)\right)\to {\phi }\right)$
7 alrot3 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{y},{z}⟩\wedge \left({y}\in {A}\wedge {z}\in {B}\right)\right)\to {\phi }\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{y},{z}⟩\wedge \left({y}\in {A}\wedge {z}\in {B}\right)\right)\to {\phi }\right)$
8 impexp ${⊢}\left(\left({x}=⟨{y},{z}⟩\wedge \left({y}\in {A}\wedge {z}\in {B}\right)\right)\to {\phi }\right)↔\left({x}=⟨{y},{z}⟩\to \left(\left({y}\in {A}\wedge {z}\in {B}\right)\to {\phi }\right)\right)$
9 8 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{y},{z}⟩\wedge \left({y}\in {A}\wedge {z}\in {B}\right)\right)\to {\phi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\to \left(\left({y}\in {A}\wedge {z}\in {B}\right)\to {\phi }\right)\right)$
10 opex ${⊢}⟨{y},{z}⟩\in \mathrm{V}$
11 1 imbi2d ${⊢}{x}=⟨{y},{z}⟩\to \left(\left(\left({y}\in {A}\wedge {z}\in {B}\right)\to {\phi }\right)↔\left(\left({y}\in {A}\wedge {z}\in {B}\right)\to {\psi }\right)\right)$
12 10 11 ceqsalv ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\to \left(\left({y}\in {A}\wedge {z}\in {B}\right)\to {\phi }\right)\right)↔\left(\left({y}\in {A}\wedge {z}\in {B}\right)\to {\psi }\right)$
13 9 12 bitri ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{y},{z}⟩\wedge \left({y}\in {A}\wedge {z}\in {B}\right)\right)\to {\phi }\right)↔\left(\left({y}\in {A}\wedge {z}\in {B}\right)\to {\psi }\right)$
14 13 2albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{y},{z}⟩\wedge \left({y}\in {A}\wedge {z}\in {B}\right)\right)\to {\phi }\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {A}\wedge {z}\in {B}\right)\to {\psi }\right)$
15 7 14 bitri ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}=⟨{y},{z}⟩\wedge \left({y}\in {A}\wedge {z}\in {B}\right)\right)\to {\phi }\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {A}\wedge {z}\in {B}\right)\to {\psi }\right)$
16 6 15 bitri ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \bigcup _{{y}\in {A}}\left(\left\{{y}\right\}×{B}\right)\to {\phi }\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {A}\wedge {z}\in {B}\right)\to {\psi }\right)$
17 df-ral ${⊢}\forall {x}\in \bigcup _{{y}\in {A}}\left(\left\{{y}\right\}×{B}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \bigcup _{{y}\in {A}}\left(\left\{{y}\right\}×{B}\right)\to {\phi }\right)$
18 r2al ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {A}\wedge {z}\in {B}\right)\to {\psi }\right)$
19 16 17 18 3bitr4i ${⊢}\forall {x}\in \bigcup _{{y}\in {A}}\left(\left\{{y}\right\}×{B}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$