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

Theorem nfel 2625
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 2621 . 2  |-  ( T. 
->  F/ x  A  e.  B )
65trud 1379 1  |-  F/ x  A  e.  B
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1371   F/wnf 1590    e. wcel 1758   F/_wnfc 2599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-cleq 2443  df-clel 2446  df-nfc 2601
This theorem is referenced by:  nfel1  2628  nfel2  2630  nfnel  2791  elabgf  3203  elrabf  3214  sbcel12  3775  sbcel12gOLD  3776  rabxfrd  4613  ffnfvf  5971  mptelixpg  7402  ac6num  8751  ptcldmpt  19305  prdsdsf  20060  prdsxmet  20062  rmo4fOLD  26017  ssiun2sf  26046  ssrelf  26081  funcnv4mpt  26125  nnindf  26225  oms0  26846  ptrest  28565  aomclem8  29554  elunif  29878  rspcegf  29885  climsuse  29921  stoweidlem59  29994  nfdfat  30176  ovmpt3rab1  30301  bnj1491  32350
  Copyright terms: Public domain W3C validator