Metamath Proof Explorer


Theorem rr-spce

Description: Prove an existential. (Contributed by Rohan Ridenour, 12-Aug-2023)

Ref Expression
Hypotheses rr-spce.1 φ x = A ψ
rr-spce.2 φ A V
Assertion rr-spce φ x ψ

Proof

Step Hyp Ref Expression
1 rr-spce.1 φ x = A ψ
2 rr-spce.2 φ A V
3 2 elexd φ A V
4 isset A V x x = A
5 3 4 sylib φ x x = A
6 1 ex φ x = A ψ
7 6 eximdv φ x x = A x ψ
8 5 7 mpd φ x ψ