Metamath Proof Explorer

Theorem 2reu5a

Description: Double restricted existential uniqueness in terms of restricted existence and restricted "at most one." (Contributed by Alexander van der Vekens, 17-Jun-2017)

Ref Expression
Assertion 2reu5a ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{y}\in {B}{\phi }\right)\wedge {\exists }^{*}{x}\in {A}\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{y}\in {B}{\phi }\right)\right)$

Proof

Step Hyp Ref Expression
1 reu5 ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{x}\in {A}\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
2 reu5 ${⊢}\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{y}\in {B}{\phi }\right)$
3 2 rexbii ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{y}\in {B}{\phi }\right)$
4 2 rmobii ${⊢}{\exists }^{*}{x}\in {A}\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔{\exists }^{*}{x}\in {A}\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{y}\in {B}{\phi }\right)$
5 3 4 anbi12i ${⊢}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{x}\in {A}\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{y}\in {B}{\phi }\right)\wedge {\exists }^{*}{x}\in {A}\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{y}\in {B}{\phi }\right)\right)$
6 1 5 bitri ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{y}\in {B}{\phi }\right)\wedge {\exists }^{*}{x}\in {A}\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{y}\in {B}{\phi }\right)\right)$