nfel1 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > nfel1		Unicode version

Theorem nfel1 2310

Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)

**Hypothesis**
Ref	Expression
nfeq1.1

**Assertion**
Ref	Expression
nfel1

(

)

**Proof of Theorem 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