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

Theorem nfel2 2464
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 2452 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfel 2460 1  |-  F/ x  A  e.  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1535    e. wcel 1701   F/_wnfc 2439
This theorem is referenced by:  elabgt  2945  opelopabsb  4312  reusv2lem4  4575  eliunxp  4860  opeliunxp2  4861  elrnmpt1  4965  tz6.12f  5584  fmpt2x  6232  riotaxfrd  6378  cbvixp  6876  boxcutc  6902  ixpiunwdom  7350  rankidb  7517  rankuni2b  7570  acni2  7718  ac6c4  8153  iundom2g  8207  tskuni  8450  fsum2dlem  12280  fsumcom2  12284  gsum2d2lem  15273  gsumcom2  15275  ptclsg  17365  prdsdsf  17983  ovoliunnul  18919  iundisj  18958  iunmbl2  18967  iundisjf  23171  iundisjfi  23301  nfcprod  24414  sdclem1  25602  0neqopab  27249  bnj1463  28596
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-cleq 2309  df-clel 2312  df-nfc 2441
  Copyright terms: Public domain W3C validator