Metamath Proof Explorer

Theorem r19.28v

Description: Restricted quantifier version of one direction of 19.28 . (The other direction holds when A is nonempty, see r19.28zv .) (Contributed by NM, 2-Apr-2004) (Proof shortened by Wolf Lammen, 17-Jun-2023)

Ref Expression
Assertion r19.28v ${⊢}\left({\phi }\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)$

Proof

Step Hyp Ref Expression
1 id ${⊢}{\phi }\to {\phi }$
2 1 ralrimivw ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
3 2 anim1i ${⊢}\left({\phi }\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
4 r19.26 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
5 3 4 sylibr ${⊢}\left({\phi }\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)$