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

Theorem nfel2 2642
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 2624 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfel 2637 1  |-  F/ x  A  e.  B
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1594    e. wcel 1762   F/_wnfc 2610
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-cleq 2454  df-clel 2457  df-nfc 2612
This theorem is referenced by:  elabgt  3242  opelopabsb  4752  eliunxp  5133  opeliunxp2  5134  tz6.12f  5877  riotaxfrd  6269  0neqopab  6318  cbvixp  7478  boxcutc  7504  ixpiunwdom  8008  rankidb  8209  rankuni2b  8262  acni2  8418  ac6c4  8852  iundom2g  8906  tskuni  9152  nfsum1  13463  nfsum  13464  gsumcom2  16789  gsummatr01lem4  18922  ptclsg  19846  cnextfvval  20295  prdsdsf  20600  ptrest  29614  mbfposadd  29628  sdclem1  29828  stoweidlem26  31283  stoweidlem36  31293  stoweidlem46  31303  stoweidlem51  31308  eliunxp2  31864  bnj1463  33067  bj-nfcf  33450
  Copyright terms: Public domain W3C validator