Theorem abexd

Description: Conditions for a class abstraction to be a set, deduction form. (Contributed by AV, 19-Apr-2025)

	Ref	Expression
Hypotheses	abexd.1	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑥 ∈ 𝐴 )
	abexd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	abexd	⊢ ( 𝜑 → { 𝑥 ∣ 𝜓 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		abexd.1	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑥 ∈ 𝐴 )
2		abexd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3	1	ex	⊢ ( 𝜑 → ( 𝜓 → 𝑥 ∈ 𝐴 ) )
4	3	alrimiv	⊢ ( 𝜑 → ∀ 𝑥 ( 𝜓 → 𝑥 ∈ 𝐴 ) )
5		abss	⊢ ( { 𝑥 ∣ 𝜓 } ⊆ 𝐴 ↔ ∀ 𝑥 ( 𝜓 → 𝑥 ∈ 𝐴 ) )
6	4 5	sylibr	⊢ ( 𝜑 → { 𝑥 ∣ 𝜓 } ⊆ 𝐴 )
7	2 6	ssexd	⊢ ( 𝜑 → { 𝑥 ∣ 𝜓 } ∈ V )