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

Theorem nfel 2642
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 2637 . 2  |-  ( T. 
->  F/ x  A  e.  B )
65trud 1388 1  |-  F/ x  A  e.  B
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1380   F/wnf 1599    e. wcel 1767   F/_wnfc 2615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-cleq 2459  df-clel 2462  df-nfc 2617
This theorem is referenced by:  nfel1  2645  nfel2  2647  nfnel  2810  elabgf  3248  elrabf  3259  sbcel12  3823  sbcel12gOLD  3824  rabxfrd  4668  ffnfvf  6046  ovmpt3rab1  6516  mptelixpg  7503  ac6num  8855  gsumsnf  16771  ptcldmpt  19850  prdsdsf  20605  prdsxmet  20607  rmo4fOLD  27071  ssiun2sf  27100  ssrelf  27139  funcnv4mpt  27184  nnindf  27278  oms0  27906  ptrest  29625  aomclem8  30611  elunif  30969  rspcegf  30976  upbdrech  31082  ssfiunibd  31086  climsuse  31150  climaddf  31157  mullimc  31158  limcperiod  31170  icccncfext  31226  iblspltprt  31291  stoweidlem59  31359  fourierdlem16  31423  fourierdlem21  31428  fourierdlem22  31429  fourierdlem31  31438  fourierdlem48  31455  fourierdlem51  31458  fourierdlem53  31460  fourierdlem80  31487  fourierdlem89  31496  fourierdlem91  31498  fourierdlem93  31500  fourierdlem112  31519  nfdfat  31682  bnj1491  33192
  Copyright terms: Public domain W3C validator