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

Theorem nfel2 2431
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 2419 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfel 2427 1  |-  F/ x  A  e.  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1531    e. wcel 1684   F/_wnfc 2406
This theorem is referenced by:  elabgt  2911  opelopabsb  4275  reusv2lem4  4538  eliunxp  4823  opeliunxp2  4824  elrnmpt1  4928  tz6.12f  5546  fmpt2x  6190  riotaxfrd  6336  cbvixp  6833  boxcutc  6859  ixpiunwdom  7305  rankidb  7472  rankuni2b  7525  acni2  7673  ac6c4  8108  iundom2g  8162  tskuni  8405  fsum2dlem  12233  fsumcom2  12237  gsum2d2lem  15224  gsumcom2  15226  ptclsg  17309  prdsdsf  17931  ovoliunnul  18866  iundisj  18905  iunmbl2  18914  iundisjfi  23363  iundisjf  23365  lineval22  26082  sdclem1  26453  bnj1463  29085
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408
  Copyright terms: Public domain W3C validator