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

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

Proof of Theorem nfel1
StepHypRef Expression
1 nfeq1.1 . 2 xA
2 nfcv 2151 . 2 xB
31, 2nfel 2159 1 x A B
Colors of variables: wff set class
Syntax hints:  wnf 1322   wcel 1366  wnfc 2138
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 614  ax-5 1309  ax-7 1310  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-10 1369  ax-11 1370  ax-i12 1371  ax-bnd 1372  ax-4 1373  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-i5r 1401  ax-ext 1995
This theorem depends on definitions:  df-bi 110  df-tru 1226  df-nf 1323  df-sb 1619  df-cleq 2006  df-clel 2009  df-nfc 2140
This theorem is referenced by:  vtocl2gf  2583  vtocl3gf  2584  vtoclgaf  2586  vtocl2gaf  2588  vtocl3gaf  2590  nfop  3528  pofun  4012  nfse  4035  rabxfrd  4139  mptfvex  5169  fvmptf  5176  fmptcof  5244  fliftfuns  5351  riota2f  5401  ovmpt2s  5535  ov2gf  5536  fmpt2x  5737  mpt2fvex  5740  qliftfuns  6089
  Copyright terms: Public domain W3C validator