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