Metamath Proof Explorer

Theorem reuanid

Description: Cancellation law for restricted unique existential quantification. (Contributed by Peter Mazsa, 12-Feb-2018)

Ref Expression
Assertion reuanid ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)↔\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$

Proof

Step Hyp Ref Expression
1 anabs5 ${⊢}\left({x}\in {A}\wedge \left({x}\in {A}\wedge {\phi }\right)\right)↔\left({x}\in {A}\wedge {\phi }\right)$
2 1 eubii ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge \left({x}\in {A}\wedge {\phi }\right)\right)↔\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
3 df-reu ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)↔\exists !{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge \left({x}\in {A}\wedge {\phi }\right)\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 2 3 4 3bitr4i ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)↔\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$