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

Theorem nfel1 2235
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 2225 . 2 𝑥𝐵
31, 2nfel 2233 1 𝑥 𝐴𝐵
Colors of variables: wff set class
Syntax hints:  wnf 1392  wcel 1436  wnfc 2212
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-cleq 2078  df-clel 2081  df-nfc 2214
This theorem is referenced by:  vtocl2gf  2674  vtocl3gf  2675  vtoclgaf  2677  vtocl2gaf  2679  vtocl3gaf  2681  nfop  3621  pofun  4112  nfse  4141  rabxfrd  4264  mptfvex  5345  fvmptf  5352  fmptcof  5422  fliftfuns  5532  riota2f  5584  ovmpt2s  5719  ov2gf  5720  fmpt2x  5921  mpt2fvex  5924  qliftfuns  6322  xpf1o  6506  sumfct  10646  isumrblem  10648  isummolem3  10652  isummolem2a  10653  zisum  10656  fisum  10658  isumss  10662  infssuzcldc  10814
  Copyright terms: Public domain W3C validator