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

Theorem nfel 2593
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 2588 . 2  |-  ( T. 
->  F/ x  A  e.  B )
65trud 1446 1  |-  F/ x  A  e.  B
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1438   F/wnf 1661    e. wcel 1872   F/_wnfc 2566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-cleq 2414  df-clel 2417  df-nfc 2568
This theorem is referenced by:  nfel1  2596  nfel2  2598  nfnel  2764  elabgf  3215  elrabf  3226  sbcel12  3802  rabxfrd  4642  ffnfvf  6066  mptelixpg  7571  ac6num  8917  fproddivf  14041  fprodsplit1f  14044  ptcldmpt  20628  prdsdsf  21381  prdsxmet  21383  rmo4fOLD  28131  iunin1f  28174  iunxsngf  28175  ssiun2sf  28177  acunirnmpt2  28265  acunirnmpt2f  28266  aciunf1lem  28267  funcnv4mpt  28276  esumc  28881  esumrnmpt2  28898  esumgect  28920  esum2dlem  28922  esum2d  28923  esumiun  28924  ldsysgenld  28991  sigapildsys  28993  fiunelros  29005  omssubadd  29137  oms0OLD  29138  omssubaddOLD  29141  bnj1491  29875  ptrest  31904  aomclem8  35890  ss2iundf  36222  sbcel12gOLD  36876  elunif  37311  rspcegf  37318  iunxsngf2  37376  fiiuncl  37380  disjf1  37419  wessf1ornlem  37421  disjrnmpt2  37425  disjf1o  37428  disjinfi  37430  iuneqfzuzlem  37512  fsumsplit1  37593  fsumiunss  37596  climsuse  37628  fprodcncf  37720  dvmptmulf  37753  dvnmptdivc  37754  dvnmul  37759  dvmptfprodlem  37760  dvmptfprod  37761  dvnprodlem1  37762  dvnprodlem2  37763  stoweidlem59  37861  fourierdlem31  37941  fourierdlem31OLD  37942  sge00  38127  sge0f1o  38133  sge0pnffigt  38147  sge0lefi  38149  sge0resplit  38157  sge0lempt  38161  sge0iunmptlemfi  38164  sge0iunmptlemre  38166  sge0iunmpt  38169  sge0xadd  38186  sge0gtfsumgt  38194  iundjiun  38207  meadjiun  38213  omeiunltfirp  38249  hoidmvlelem1  38322  hoidmvlelem3  38324  nfdfat  38503
  Copyright terms: Public domain W3C validator