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

Theorem nfel2 2950
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 2934 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfel 2946 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1827  wcel 2107  wnfc 2919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-cleq 2770  df-clel 2774  df-nfc 2921
This theorem is referenced by:  elabgt  3553  elabg  3556  opelopabsb  5222  eliunxp  5505  opeliunxp2  5506  tz6.12f  6470  riotaxfrd  6914  0neqopab  6975  opeliunxp2f  7618  cbvixp  8211  boxcutc  8237  ixpiunwdom  8785  rankidb  8960  rankuni2b  9013  acni2  9202  ac6c4  9638  iundom2g  9697  tskuni  9940  reuccats1OLD  13848  reuccatpfxs1  13883  gsumcom2  18760  gsummatr01lem4  20870  ptclsg  21827  cnextfvval  22277  prdsdsf  22580  nnindf  30129  bnj1463  31722  ptrest  34034  sdclem1  34163  eqrelf  34655  binomcxplemnotnn0  39511  eliin2f  40216  stoweidlem26  41170  stoweidlem36  41180  stoweidlem46  41190  stoweidlem51  41195  eliunxp2  43127  setrec1  43543
  Copyright terms: Public domain W3C validator