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

Theorem nfel2 2628
Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq2.1  |-  F/_ x B
Assertion
Ref Expression
nfel2  |-  F/ x  A  e.  B
Distinct variable group:    x, A
Allowed substitution hint:    B( x)

Proof of Theorem nfel2
StepHypRef Expression
1 nfcv 2612 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfel 2624 1  |-  F/ x  A  e.  B
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1675    e. wcel 1904   F/_wnfc 2599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-cleq 2464  df-clel 2467  df-nfc 2601
This theorem is referenced by:  elabgt  3170  opelopabsb  4711  eliunxp  4977  opeliunxp2  4978  tz6.12f  5897  riotaxfrd  6300  0neqopab  6353  opeliunxp2f  6975  cbvixp  7557  boxcutc  7583  ixpiunwdom  8124  rankidb  8289  rankuni2b  8342  acni2  8495  ac6c4  8929  iundom2g  8983  tskuni  9226  gsumcom2  17685  gsummatr01lem4  19760  ptclsg  20707  cnextfvval  21158  prdsdsf  21460  nnindf  28457  bnj1463  29936  ptrest  32003  sdclem1  32136  binomcxplemnotnn0  36775  stoweidlem26  37998  stoweidlem36  38009  stoweidlem46  38019  stoweidlem51  38024  eliunxp2  40623
  Copyright terms: Public domain W3C validator