Theorem rr-spce

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

	Ref	Expression
Hypotheses	rr-spce.1	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝜓 )
	rr-spce.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	rr-spce	⊢ ( 𝜑 → ∃ 𝑥 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		rr-spce.1	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝜓 )
2		rr-spce.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3	2	elexd	⊢ ( 𝜑 → 𝐴 ∈ V )
4		isset	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 )
5	3 4	sylib	⊢ ( 𝜑 → ∃ 𝑥 𝑥 = 𝐴 )
6	1	ex	⊢ ( 𝜑 → ( 𝑥 = 𝐴 → 𝜓 ) )
7	6	eximdv	⊢ ( 𝜑 → ( ∃ 𝑥 𝑥 = 𝐴 → ∃ 𝑥 𝜓 ) )
8	5 7	mpd	⊢ ( 𝜑 → ∃ 𝑥 𝜓 )