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

Theorem nfel2 2924
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 2905 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfel 2920 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1783  wcel 2108  wnfc 2890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2729  df-clel 2816  df-nfc 2892
This theorem is referenced by:  eliunxp  5848  opeliunxp2  5849  tz6.12f  6932  riotaxfrd  7422  opeliunxp2f  8235  cbvixp  8954  boxcutc  8981  ixpiunwdom  9630  rankidb  9840  rankuni2b  9893  acni2  10086  ac6c4  10521  iundom2g  10580  tskuni  10823  reuccatpfxs1  14785  gsumcom2  19993  gsummatr01lem4  22664  ptclsg  23623  cnextfvval  24073  prdsdsf  24377  nnindf  32821  gsumpart  33060  nsgqusf1olem1  33441  nsgqusf1olem3  33443  bnj1463  35069  fineqvrep  35109  ptrest  37626  sdclem1  37750  eqrelf  38256  binomcxplemnotnn0  44375  eliin2f  45109  stoweidlem26  46041  stoweidlem36  46051  stoweidlem46  46061  stoweidlem51  46066  sge0f1o  46397  finfdm  46861  eliunxp2  48250  setrec1  49210
  Copyright terms: Public domain W3C validator