Metamath Proof Explorer

Theorem cjex

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

Ref Expression
Assertion cjex 
|- * e. _V

Proof

Step Hyp Ref Expression
1 cjf 
 |-  * : CC --> CC
2 cnex 
 |-  CC e. _V
3 fex2 
 |-  ( ( * : CC --> CC /\ CC e. _V /\ CC e. _V ) -> * e. _V )
4 1 2 2 3 mp3an 
 |-  * e. _V