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

Theorem nfel1 2267
Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq1.1  |-  F/_ x A
Assertion
Ref Expression
nfel1  |-  F/ x  A  e.  B
Distinct variable group:    x, B
Allowed substitution hint:    A( x)

Proof of Theorem nfel1
StepHypRef Expression
1 nfeq1.1 . 2  |-  F/_ x A
2 nfcv 2256 . 2  |-  F/_ x B
31, 2nfel 2265 1  |-  F/ x  A  e.  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1419    e. wcel 1463   F/_wnfc 2243
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-cleq 2108  df-clel 2111  df-nfc 2245
This theorem is referenced by:  vtocl2gf  2720  vtocl3gf  2721  vtoclgaf  2723  vtocl2gaf  2725  vtocl3gaf  2727  nfop  3689  pofun  4202  nfse  4231  rabxfrd  4358  mptfvex  5472  fvmptf  5479  fmptcof  5553  fliftfuns  5665  riota2f  5717  ovmpos  5860  ov2gf  5861  fmpox  6064  mpofvex  6067  qliftfuns  6479  xpf1o  6704  iunfidisj  6800  sumfct  11083  sumrbdclem  11085  summodclem3  11089  summodclem2a  11090  zsumdc  11093  fsumgcl  11095  fsum3  11096  isumss  11100  isumss2  11102  fsum3cvg2  11103  fsumsplitf  11117  fsum2dlemstep  11143  fisumcom2  11147  fsumshftm  11154  fisum0diag2  11156  fsummulc2  11157  fsum00  11171  fsumabs  11174  fsumrelem  11180  fsumiun  11186  isumshft  11199  mertenslem2  11245  infssuzcldc  11540  iuncld  12179  fsumcncntop  12620
  Copyright terms: Public domain W3C validator