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

Metamath Proof Explorer

Theorem cjex

Description: The conjugate function is a set. (Contributed by SN, 5-Jun-2025)

Ref Expression
Assertion cjex ∗ ∈ V

Proof

Step Hyp Ref Expression
1 cjf ⊢ ∗ : ℂ ⟶ ℂ
2 cnex ⊢ ℂ ∈ V
3 fex2 ⊢ ( ( ∗ : ℂ ⟶ ℂ ∧ ℂ ∈ V ∧ ℂ ∈ V ) → ∗ ∈ V )
4 1 2 2 3 mp3an ⊢ ∗ ∈ V