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

Theorem nfel2 2777
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 2761 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfel 2773 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1705  wcel 1987  wnfc 2748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-cleq 2614  df-clel 2617  df-nfc 2750
This theorem is referenced by:  elabgt  3331  opelopabsb  4947  eliunxp  5221  opeliunxp2  5222  tz6.12f  6171  riotaxfrd  6599  0neqopab  6654  opeliunxp2f  7284  cbvixp  7872  boxcutc  7898  ixpiunwdom  8443  rankidb  8610  rankuni2b  8663  acni2  8816  ac6c4  9250  iundom2g  9309  tskuni  9552  gsumcom2  18298  gsummatr01lem4  20386  ptclsg  21331  cnextfvval  21782  prdsdsf  22085  nnindf  29418  bnj1463  30852  ptrest  33061  sdclem1  33192  binomcxplemnotnn0  38058  eliin2f  38791  stoweidlem26  39566  stoweidlem36  39576  stoweidlem46  39586  stoweidlem51  39591  eliunxp2  41416  setrec1  41747
  Copyright terms: Public domain W3C validator