| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | GIF version | ||
| Description: Alias for ax-cnex 8271. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex | ⊢ ℂ ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 8271 | 1 ⊢ ℂ ∈ V |
| Colors of variables: wff set class |
| This proof depends on syntax axioms: ∈ wcel 2209 Vcvv 2821 ℂcc 8178 |
| This proof depends on axioms: ax-cnex 8271 |
| This theorem is used by: reex 8314 cnelprrecn 8316 pnfnre 8368 mnfnre 8369 pnfxr 8379 nnex 9313 zex 9658 qex 10042 addex 10063 mulex 10064 ovshftex 11600 cndsex 14974 cnfldstr 14979 cnfldbas 14981 mpocnfldadd 14982 mpocnfldmul 14984 cnfldcj 14986 expghmap 15026 lmfval 15385 lmbrf 15407 lmfss 15436 lmres 15440 lmtopcnp 15442 cnmet 15722 cncfval 15764 elcncf 15765 limcrcl 15850 limccl 15851 ellimc3apf 15852 limccnp2lem 15868 limccnp2cntop 15869 reldvg 15871 dvfvalap 15873 dvbss 15877 dvidlemap 15883 dvidrelem 15884 dvidsslem 15885 dvcnp2cntop 15891 dvaddxxbr 15893 dvmulxxbr 15894 dvaddxx 15895 dvmulxx 15896 dviaddf 15897 dvimulf 15898 dvcoapbr 15899 dvcjbr 15900 dvcj 15901 dvfre 15902 dvexp 15903 dvrecap 15905 dvmptclx 15910 dvef 15919 plyval 15924 elply 15926 elply2 15927 plyf 15929 plyss 15930 elplyr 15932 plyaddlem1 15939 plymullem1 15940 plyaddlem 15941 plymullem 15942 plysub 15945 plycolemc 15950 plyco 15951 plycj 15953 |
| Copyright terms: Public domain | W3C validator |