# Metamath Proof Explorer

## Theorem reubiia

Description: Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 14-Nov-2004)

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

### Proof

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