Metamath Proof Explorer


Theorem reuun1

Description: Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005)

Ref Expression
Assertion reuun1 ( ( ∃ 𝑥𝐴 𝜑 ∧ ∃! 𝑥 ∈ ( 𝐴𝐵 ) ( 𝜑𝜓 ) ) → ∃! 𝑥𝐴 𝜑 )

Proof

Step Hyp Ref Expression
1 ssun1 𝐴 ⊆ ( 𝐴𝐵 )
2 orc ( 𝜑 → ( 𝜑𝜓 ) )
3 2 rgenw 𝑥𝐴 ( 𝜑 → ( 𝜑𝜓 ) )
4 reuss2 ( ( ( 𝐴 ⊆ ( 𝐴𝐵 ) ∧ ∀ 𝑥𝐴 ( 𝜑 → ( 𝜑𝜓 ) ) ) ∧ ( ∃ 𝑥𝐴 𝜑 ∧ ∃! 𝑥 ∈ ( 𝐴𝐵 ) ( 𝜑𝜓 ) ) ) → ∃! 𝑥𝐴 𝜑 )
5 1 3 4 mpanl12 ( ( ∃ 𝑥𝐴 𝜑 ∧ ∃! 𝑥 ∈ ( 𝐴𝐵 ) ( 𝜑𝜓 ) ) → ∃! 𝑥𝐴 𝜑 )