Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfel1 | Unicode version |
Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
Ref | Expression |
---|---|
nfeq1.1 |
Ref | Expression |
---|---|
nfel1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfeq1.1 | . 2 | |
2 | nfcv 2299 | . 2 | |
3 | 1, 2 | nfel 2308 | 1 |
Colors of variables: wff set class |
Syntax hints: wnf 1440 wcel 2128 wnfc 2286 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-tru 1338 df-nf 1441 df-sb 1743 df-cleq 2150 df-clel 2153 df-nfc 2288 |
This theorem is referenced by: vtocl2gf 2774 vtocl3gf 2775 vtoclgaf 2777 vtocl2gaf 2779 vtocl3gaf 2781 nfop 3757 pofun 4272 nfse 4301 rabxfrd 4429 mptfvex 5553 fvmptf 5560 fmptcof 5634 fliftfuns 5748 riota2f 5801 ovmpos 5944 ov2gf 5945 fmpox 6148 mpofvex 6151 qliftfuns 6564 xpf1o 6789 iunfidisj 6890 cc3 7188 sumfct 11271 sumrbdclem 11274 summodclem3 11277 summodclem2a 11278 zsumdc 11281 fsumgcl 11283 fsum3 11284 isumss 11288 isumss2 11290 fsum3cvg2 11291 fsumsplitf 11305 fsum2dlemstep 11331 fisumcom2 11335 fsumshftm 11342 fisum0diag2 11344 fsummulc2 11345 fsum00 11359 fsumabs 11362 fsumrelem 11368 fsumiun 11374 isumshft 11387 mertenslem2 11433 prodrbdclem 11468 prodmodclem3 11472 prodmodclem2a 11473 zproddc 11476 fprodseq 11480 prodfct 11484 prodssdc 11486 fprodmul 11488 fprodm1s 11498 fprodp1s 11499 fprodcl2lem 11502 fprodabs 11513 fprod2dlemstep 11519 fprodcom2fi 11523 fprodrec 11526 fproddivapf 11528 fprodsplitf 11529 fprodsplit1f 11531 fprodle 11537 infssuzcldc 11838 iuncld 12526 fsumcncntop 12967 |
Copyright terms: Public domain | W3C validator |