Metamath Proof Explorer


Theorem reubii

Description: Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 22-Oct-1999)

Ref Expression
Hypothesis reubii.1 φψ
Assertion reubii ∃!xAφ∃!xAψ

Proof

Step Hyp Ref Expression
1 reubii.1 φψ
2 1 a1i xAφψ
3 2 reubiia ∃!xAφ∃!xAψ