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

Metamath Proof Explorer

Theorem qsex

Description: A quotient set exists. (Contributed by NM, 14-Aug-1995)

Ref Expression
Hypothesis qsex.1 ⊢ 𝐴 ∈ V
Assertion qsex ( 𝐴 / 𝑅 ) ∈ V

Proof

Step Hyp Ref Expression
1 qsex.1 ⊢ 𝐴 ∈ V
2 qsexg ⊢ ( 𝐴 ∈ V → ( 𝐴 / 𝑅 ) ∈ V )
3 1 2 ax-mp ⊢ ( 𝐴 / 𝑅 ) ∈ V