MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfel2 Structured version   Visualization version   GIF version

Theorem nfel2 2930
Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq2.1 𝑥𝐵
Assertion
Ref Expression
nfel2 𝑥 𝐴𝐵
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem nfel2
StepHypRef Expression
1 nfcv 2913 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfel 2926 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1856  wcel 2145  wnfc 2900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-cleq 2764  df-clel 2767  df-nfc 2902
This theorem is referenced by:  elabgt  3498  opelopabsb  5118  eliunxp  5398  opeliunxp2  5399  tz6.12f  6353  riotaxfrd  6785  0neqopab  6845  opeliunxp2f  7488  cbvixp  8079  boxcutc  8105  ixpiunwdom  8652  rankidb  8827  rankuni2b  8880  acni2  9069  ac6c4  9505  iundom2g  9564  tskuni  9807  reuccats1  13689  gsumcom2  18581  gsummatr01lem4  20683  ptclsg  21639  cnextfvval  22089  prdsdsf  22392  nnindf  29905  bnj1463  31461  ptrest  33741  sdclem1  33871  eqrelf  34363  binomcxplemnotnn0  39081  eliin2f  39808  stoweidlem26  40760  stoweidlem36  40770  stoweidlem46  40780  stoweidlem51  40785  eliunxp2  42640  setrec1  42966
  Copyright terms: Public domain W3C validator