Metamath Proof Explorer

Theorem ralunsn

Description: Restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012) (Revised by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypothesis ralunsn.1 ${⊢}{x}={B}\to \left({\phi }↔{\psi }\right)$
Assertion ralunsn ${⊢}{B}\in {C}\to \left(\forall {x}\in \left({A}\cup \left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)\right)$

Proof

Step Hyp Ref Expression
1 ralunsn.1 ${⊢}{x}={B}\to \left({\phi }↔{\psi }\right)$
2 ralunb ${⊢}\forall {x}\in \left({A}\cup \left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\in \left\{{B}\right\}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
3 1 ralsng ${⊢}{B}\in {C}\to \left(\forall {x}\in \left\{{B}\right\}\phantom{\rule{.4em}{0ex}}{\phi }↔{\psi }\right)$
4 3 anbi2d ${⊢}{B}\in {C}\to \left(\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\in \left\{{B}\right\}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)\right)$
5 2 4 syl5bb ${⊢}{B}\in {C}\to \left(\forall {x}\in \left({A}\cup \left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\psi }\right)\right)$