| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > nfel1 | GIF 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 2348 | . 2 ⊢ Ⅎ𝑥𝐵 | |
| 3 | 1, 2 | nfel 2357 | 1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 |
| Colors of variables: wff set class |
| Syntax hints: Ⅎwnf 1483 ∈ wcel 2176 Ⅎwnfc 2335 |
| 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 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-ext 2187 |
| This theorem depends on definitions: df-bi 117 df-tru 1376 df-nf 1484 df-sb 1786 df-cleq 2198 df-clel 2201 df-nfc 2337 |
| This theorem is referenced by: vtocl2gf 2835 vtocl3gf 2836 vtoclgaf 2838 vtocl2gaf 2840 vtocl3gaf 2842 nfop 3835 pofun 4359 nfse 4388 rabxfrd 4516 mptfvex 5665 fvmptf 5672 fmptcof 5747 fliftfuns 5867 riota2f 5921 ovmpos 6069 ov2gf 6070 elovmporab 6146 elovmporab1w 6147 fmpox 6286 mpofvex 6291 qliftfuns 6706 xpf1o 6941 iunfidisj 7048 cc3 7380 infssuzcldc 10378 sumfct 11685 sumrbdclem 11688 summodclem3 11691 summodclem2a 11692 zsumdc 11695 fsumgcl 11697 fsum3 11698 isumss 11702 isumss2 11704 fsum3cvg2 11705 fsumsplitf 11719 fsum2dlemstep 11745 fisumcom2 11749 fsumshftm 11756 fisum0diag2 11758 fsummulc2 11759 fsum00 11773 fsumabs 11776 fsumrelem 11782 fsumiun 11788 isumshft 11801 mertenslem2 11847 prodrbdclem 11882 prodmodclem3 11886 prodmodclem2a 11887 zproddc 11890 fprodseq 11894 prodfct 11898 prodssdc 11900 fprodmul 11902 fprodm1s 11912 fprodp1s 11913 fprodcl2lem 11916 fprodabs 11927 fprod2dlemstep 11933 fprodcom2fi 11937 fprodrec 11940 fproddivapf 11942 fprodsplitf 11943 fprodsplit1f 11945 fprodle 11951 pcmpt 12666 pcmptdvds 12668 gsumfzfsumlemm 14349 iuncld 14587 fsumcncntop 15039 dvmptfsum 15197 |
| Copyright terms: Public domain | W3C validator |