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

Theorem nfel2 2582
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 2564 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfel 2577 1  |-  F/ x  A  e.  B
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1637    e. wcel 1842   F/_wnfc 2550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-cleq 2394  df-clel 2397  df-nfc 2552
This theorem is referenced by:  elabgt  3192  opelopabsb  4699  eliunxp  5082  opeliunxp2  5083  tz6.12f  5823  riotaxfrd  6226  0neqopab  6278  cbvixp  7444  boxcutc  7470  ixpiunwdom  7971  rankidb  8170  rankuni2b  8223  acni2  8379  ac6c4  8813  iundom2g  8867  tskuni  9111  gsumcom2  17216  gsummatr01lem4  19344  ptclsg  20300  cnextfvval  20749  prdsdsf  21054  nnindf  27941  bnj1463  29319  ptrest  31401  sdclem1  31499  binomcxplemnotnn0  36090  stoweidlem26  37158  stoweidlem36  37168  stoweidlem46  37178  stoweidlem51  37183  eliunxp2  38414
  Copyright terms: Public domain W3C validator