# Metamath Proof Explorer

## Theorem reubidva

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 13-Nov-2004) Reduce axiom usage. (Revised by Wolf Lammen, 14-Jan-2023)

Ref Expression
Hypothesis reubidva.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({\psi }↔{\chi }\right)$
Assertion reubidva ${⊢}{\phi }\to \left(\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\chi }\right)$

### Proof

Step Hyp Ref Expression
1 reubidva.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({\psi }↔{\chi }\right)$
2 1 pm5.32da ${⊢}{\phi }\to \left(\left({x}\in {A}\wedge {\psi }\right)↔\left({x}\in {A}\wedge {\chi }\right)\right)$
3 2 eubidv ${⊢}{\phi }\to \left(\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\psi }\right)↔\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\chi }\right)\right)$
4 df-reu ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\psi }\right)$
5 df-reu ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\chi }↔\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\chi }\right)$
6 3 4 5 3bitr4g ${⊢}{\phi }\to \left(\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\chi }\right)$