Metamath Proof Explorer


Theorem reuun1

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

Ref Expression
Assertion reuun1 xAφ∃!xABφψ∃!xAφ

Proof

Step Hyp Ref Expression
1 ssun1 AAB
2 orc φφψ
3 2 rgenw xAφφψ
4 reuss2 AABxAφφψxAφ∃!xABφψ∃!xAφ
5 1 3 4 mpanl12 xAφ∃!xABφψ∃!xAφ