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

Theorem nfel2 2630
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 2613 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfel 2625 1  |-  F/ x  A  e.  B
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1590    e. wcel 1758   F/_wnfc 2599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-cleq 2443  df-clel 2446  df-nfc 2601
This theorem is referenced by:  elabgt  3200  opelopabsb  4697  eliunxp  5075  opeliunxp2  5076  tz6.12f  5807  riotaxfrd  6182  0neqopab  6230  cbvixp  7380  boxcutc  7406  ixpiunwdom  7907  rankidb  8108  rankuni2b  8161  acni2  8317  ac6c4  8751  iundom2g  8805  tskuni  9051  nfsum1  13269  nfsum  13270  gsumcom2  16572  gsummatr01lem4  18580  ptclsg  19304  cnextfvval  19753  prdsdsf  20058  ptrest  28563  mbfposadd  28577  sdclem1  28777  stoweidlem26  29959  stoweidlem36  29969  stoweidlem46  29979  stoweidlem51  29984  eliunxp2  30859  bnj1463  32346  bj-nfcf  32727
  Copyright terms: Public domain W3C validator