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
Assertion
Ref Expression
nfel1
Distinct variable group:   ,
Allowed substitution hint:   ()

Proof of Theorem nfel1
StepHypRef Expression
1 nfeq1.1 . 2
2 nfcv 2220 . 2
31, 2nfel 2228 1
 Colors of variables: wff set class Syntax hints:  wnf 1390   wcel 1434  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