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

Theorem nfel1 2230
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 2220 . 2  |-  F/_ x B
31, 2nfel 2228 1  |-  F/ x  A  e.  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1390    e. wcel 1434   F/_wnfc 2207
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-cleq 2075  df-clel 2078  df-nfc 2209
This theorem is referenced by:  vtocl2gf  2661  vtocl3gf  2662  vtoclgaf  2664  vtocl2gaf  2666  vtocl3gaf  2668  nfop  3594  pofun  4075  nfse  4104  rabxfrd  4227  mptfvex  5288  fvmptf  5295  fmptcof  5363  fliftfuns  5469  riota2f  5520  ovmpt2s  5655  ov2gf  5656  fmpt2x  5857  mpt2fvex  5860  qliftfuns  6256  xpf1o  6385  infssuzcldc  10491
  Copyright terms: Public domain W3C validator