![]() |
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 2319 |
. 2
![]() ![]() ![]() ![]() | |
3 | 1, 2 | nfel 2328 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-cleq 2170 df-clel 2173 df-nfc 2308 |
This theorem is referenced by: vtocl2gf 2800 vtocl3gf 2801 vtoclgaf 2803 vtocl2gaf 2805 vtocl3gaf 2807 nfop 3795 pofun 4313 nfse 4342 rabxfrd 4470 mptfvex 5602 fvmptf 5609 fmptcof 5684 fliftfuns 5799 riota2f 5852 ovmpos 5998 ov2gf 5999 fmpox 6201 mpofvex 6204 qliftfuns 6619 xpf1o 6844 iunfidisj 6945 cc3 7267 sumfct 11382 sumrbdclem 11385 summodclem3 11388 summodclem2a 11389 zsumdc 11392 fsumgcl 11394 fsum3 11395 isumss 11399 isumss2 11401 fsum3cvg2 11402 fsumsplitf 11416 fsum2dlemstep 11442 fisumcom2 11446 fsumshftm 11453 fisum0diag2 11455 fsummulc2 11456 fsum00 11470 fsumabs 11473 fsumrelem 11479 fsumiun 11485 isumshft 11498 mertenslem2 11544 prodrbdclem 11579 prodmodclem3 11583 prodmodclem2a 11584 zproddc 11587 fprodseq 11591 prodfct 11595 prodssdc 11597 fprodmul 11599 fprodm1s 11609 fprodp1s 11610 fprodcl2lem 11613 fprodabs 11624 fprod2dlemstep 11630 fprodcom2fi 11634 fprodrec 11637 fproddivapf 11639 fprodsplitf 11640 fprodsplit1f 11642 fprodle 11648 infssuzcldc 11952 pcmpt 12341 pcmptdvds 12343 iuncld 13618 fsumcncntop 14059 |
Copyright terms: Public domain | W3C validator |