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

Theorem nfra1 2771
Description:  x is not free in  A. x  e.  A ph. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)
Assertion
Ref Expression
nfra1  |-  F/ x A. x  e.  A  ph

Proof of Theorem nfra1
StepHypRef Expression
1 df-ral 2725 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 nfa1 1831 . 2  |-  F/ x A. x ( x  e.  A  ->  ph )
31, 2nfxfr 1615 1  |-  F/ x A. x  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1367   F/wnf 1589    e. wcel 1756   A.wral 2720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-nf 1590  df-ral 2725
This theorem is referenced by:  nfra2  2775  r19.12  2835  ralbi  2858  ralcom2  2890  nfss  3354  rspn0  3654  ralidm  3788  nfii1  4206  dfiun2g  4207  mpteq12f  4373  reusv1  4497  reusv2lem1  4498  reusv2lem2  4499  reusv2lem3  4500  reusv6OLD  4508  ralxfrALT  4516  fvmptss  5787  ffnfv  5874  riota5f  6082  mpt2eq123  6150  tfinds  6475  peano5  6504  fun11iun  6542  zfrep6  6550  tfr3  6863  tz7.48-1  6903  tz7.49  6905  nfixp1  7288  nneneq  7499  scottex  8097  dfac2  8305  infpssrlem4  8480  hsmexlem2  8601  hsmexlem4  8603  domtriomlem  8616  axdc3lem2  8625  axdc3lem4  8627  axdc4lem  8629  zorn2lem5  8674  konigthlem  8737  eltsk2g  8923  dedekind  9538  dedekindle  9539  lble  10287  mreiincl  14539  mreexexd  14591  catpropd  14653  acsmapd  15353  gsummatr01lem4  18469  bwthOLD  19019  alexsubALTlem3  19626  isucn2  19859  mptelee  23146  chirred  25804  abrexss  25898  nn0min  26095  isarchiofld  26290  ordtconlem1  26359  esumcl  26491  measvunilem  26631  measvunilem0  26632  measvuni  26633  voliune  26650  volfiniune  26651  prodeq2ii  27431  dfon2lem3  27603  trpredmintr  27700  wfrlem4  27732  frrlem4  27776  heicant  28431  cover2  28612  upixp  28628  indexdom  28633  filbcmb  28639  mzpexpmpt  29086  fnchoice  29756  rfcnnnub  29763  infrglb  29776  climsuse  29786  stoweidlem16  29816  stoweidlem28  29828  stoweidlem29  29829  stoweidlem31  29831  stoweidlem35  29835  stoweidlem48  29848  stoweidlem51  29851  stoweidlem52  29852  stoweidlem53  29853  stoweidlem54  29854  stoweidlem56  29856  stoweidlem57  29857  stoweidlem59  29859  stoweidlem60  29860  stoweidlem62  29862  wallispilem3  29867  stirlinglem13  29886  2reu1  30015  2reu4a  30018  ffnafv  30082  fsuppmapnn0fiublem  30803  fsuppmapnn0fiub  30804  fsuppmapnn0fiubex  30805  ssralv2  31241  tratrb  31247  bnj1366  31828  bnj1379  31829  bnj571  31904  bnj1039  31967  bnj1128  31986  bnj1204  32008  bnj1279  32014  bnj1307  32019  bnj1388  32029  bnj1398  32030  bnj1444  32039  bnj1489  32052  bnj1525  32065  riotasvd  32612  riotasv2d  32613  riotasv2s  32614  glbconxN  33027  pmapglbx  33418  pmapglb2xN  33421  cdleme26ee  34009  cdlemefr29exN  34051  cdlemefs32sn1aw  34063  cdleme43fsv1snlem  34069  cdleme41sn3a  34082  cdleme32d  34093  cdleme32f  34095  cdleme40m  34116  cdleme40n  34117  cdlemk36  34562  cdlemk38  34564  cdlemkid  34585  cdlemk19x  34592  cdlemk11t  34595
  Copyright terms: Public domain W3C validator