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 2312 | . 2 | |
3 | 1, 2 | nfel 2321 | 1 |
Colors of variables: wff set class |
Syntax hints: wnf 1453 wcel 2141 wnfc 2299 |
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 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-sb 1756 df-cleq 2163 df-clel 2166 df-nfc 2301 |
This theorem is referenced by: vtocl2gf 2792 vtocl3gf 2793 vtoclgaf 2795 vtocl2gaf 2797 vtocl3gaf 2799 nfop 3781 pofun 4297 nfse 4326 rabxfrd 4454 mptfvex 5581 fvmptf 5588 fmptcof 5663 fliftfuns 5777 riota2f 5830 ovmpos 5976 ov2gf 5977 fmpox 6179 mpofvex 6182 qliftfuns 6597 xpf1o 6822 iunfidisj 6923 cc3 7230 sumfct 11337 sumrbdclem 11340 summodclem3 11343 summodclem2a 11344 zsumdc 11347 fsumgcl 11349 fsum3 11350 isumss 11354 isumss2 11356 fsum3cvg2 11357 fsumsplitf 11371 fsum2dlemstep 11397 fisumcom2 11401 fsumshftm 11408 fisum0diag2 11410 fsummulc2 11411 fsum00 11425 fsumabs 11428 fsumrelem 11434 fsumiun 11440 isumshft 11453 mertenslem2 11499 prodrbdclem 11534 prodmodclem3 11538 prodmodclem2a 11539 zproddc 11542 fprodseq 11546 prodfct 11550 prodssdc 11552 fprodmul 11554 fprodm1s 11564 fprodp1s 11565 fprodcl2lem 11568 fprodabs 11579 fprod2dlemstep 11585 fprodcom2fi 11589 fprodrec 11592 fproddivapf 11594 fprodsplitf 11595 fprodsplit1f 11597 fprodle 11603 infssuzcldc 11906 pcmpt 12295 pcmptdvds 12297 iuncld 12909 fsumcncntop 13350 |
Copyright terms: Public domain | W3C validator |