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

Theorem nfel 2632
Description: Hypothesis builder for elementhood. (Contributed by NM, 1-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
Hypotheses
Ref Expression
nfnfc.1  |-  F/_ x A
nfeq.2  |-  F/_ x B
Assertion
Ref Expression
nfel  |-  F/ x  A  e.  B

Proof of Theorem nfel
StepHypRef Expression
1 nfnfc.1 . . . 4  |-  F/_ x A
21a1i 11 . . 3  |-  ( T. 
->  F/_ x A )
3 nfeq.2 . . . 4  |-  F/_ x B
43a1i 11 . . 3  |-  ( T. 
->  F/_ x B )
52, 4nfeld 2627 . 2  |-  ( T. 
->  F/ x  A  e.  B )
65trud 1404 1  |-  F/ x  A  e.  B
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1396   F/wnf 1617    e. wcel 1819   F/_wnfc 2605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-cleq 2449  df-clel 2452  df-nfc 2607
This theorem is referenced by:  nfel1  2635  nfel2  2637  nfnel  2800  elabgf  3244  elrabf  3255  sbcel12  3832  sbcel12gOLD  3833  rabxfrd  4677  ffnfvf  6059  mptelixpg  7525  ac6num  8876  ptcldmpt  20240  prdsdsf  20995  prdsxmet  20997  rmo4fOLD  27521  iunin1f  27560  iunxsngf  27561  ssiun2sf  27563  acunirnmpt2  27648  acunirnmpt2f  27649  aciunf1lem  27650  funcnv4mpt  27660  esumc  28217  esum2dlem  28252  esum2d  28253  esumiun  28254  oms0  28429  omssubadd  28432  ptrest  30210  aomclem8  31169  elunif  31552  rspcegf  31559  fsumsplit1  31734  fproddivf  31749  fprodsplit1f  31754  climsuse  31775  fprodcncf  31865  dvmptmulf  31895  dvnmptdivc  31896  dvnmul  31901  dvmptfprodlem  31902  dvmptfprod  31903  dvnprodlem1  31904  dvnprodlem2  31905  stoweidlem59  32002  fourierdlem31  32081  nfdfat  32376  bnj1491  34214
  Copyright terms: Public domain W3C validator