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 2258 | . 2 | |
3 | 1, 2 | nfel 2267 | 1 |
Colors of variables: wff set class |
Syntax hints: wnf 1421 wcel 1465 wnfc 2245 |
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 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 df-sb 1721 df-cleq 2110 df-clel 2113 df-nfc 2247 |
This theorem is referenced by: vtocl2gf 2722 vtocl3gf 2723 vtoclgaf 2725 vtocl2gaf 2727 vtocl3gaf 2729 nfop 3691 pofun 4204 nfse 4233 rabxfrd 4360 mptfvex 5474 fvmptf 5481 fmptcof 5555 fliftfuns 5667 riota2f 5719 ovmpos 5862 ov2gf 5863 fmpox 6066 mpofvex 6069 qliftfuns 6481 xpf1o 6706 iunfidisj 6802 sumfct 11098 sumrbdclem 11100 summodclem3 11104 summodclem2a 11105 zsumdc 11108 fsumgcl 11110 fsum3 11111 isumss 11115 isumss2 11117 fsum3cvg2 11118 fsumsplitf 11132 fsum2dlemstep 11158 fisumcom2 11162 fsumshftm 11169 fisum0diag2 11171 fsummulc2 11172 fsum00 11186 fsumabs 11189 fsumrelem 11195 fsumiun 11201 isumshft 11214 mertenslem2 11260 infssuzcldc 11556 iuncld 12195 fsumcncntop 12636 |
Copyright terms: Public domain | W3C validator |