This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 abssdv ⊢ ( 𝜑 → { 𝑥 ∣ 𝜓 } ⊆ 𝐴 )
5 2 4 ssexd ⊢ ( 𝜑 → { 𝑥 ∣ 𝜓 } ∈ V )