# Metamath Proof Explorer

## Theorem reuss

Description: Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999)

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

### Proof

Step Hyp Ref Expression
1 id ${⊢}{\phi }\to {\phi }$
2 1 rgenw ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)$
3 reuss2 ${⊢}\left(\left({A}\subseteq {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\right)\wedge \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\to \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
4 2 3 mpanl2 ${⊢}\left({A}\subseteq {B}\wedge \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\to \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
5 4 3impb ${⊢}\left({A}\subseteq {B}\wedge \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$