Metamath Proof Explorer


Theorem rmobii

Description: Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 16-Jun-2017)

Ref Expression
Hypothesis rmobii.1 φψ
Assertion rmobii *xAφ*xAψ

Proof

Step Hyp Ref Expression
1 rmobii.1 φψ
2 1 a1i xAφψ
3 2 rmobiia *xAφ*xAψ