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

Theorem nfra1 2785
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 2761 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 nfa1 1999 . 2  |-  F/ x A. x ( x  e.  A  ->  ph )
31, 2nfxfr 1704 1  |-  F/ x A. x  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1450   F/wnf 1675    e. wcel 1904   A.wral 2756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-12 1950
This theorem depends on definitions:  df-bi 190  df-ex 1672  df-nf 1676  df-ral 2761
This theorem is referenced by:  hbra1  2786  nfra2  2790  r19.12  2903  ralbi  2908  ralcom2  2941  nfss  3411  rspn0  3735  ralidm  3864  nfii1  4300  dfiun2g  4301  mpteq12f  4472  reusv1  4601  reusv2lem1  4602  reusv2lem2  4603  reusv2lem3  4604  ralxfrALT  4619  fvmptss  5973  ffnfv  6064  riota5f  6294  mpt2eq123  6369  tfinds  6705  peano5  6735  fun11iun  6772  zfrep6  6780  wfrlem4  7057  tfr3  7135  tz7.48-1  7178  tz7.49  7180  nfixp1  7560  nneneq  7773  scottex  8374  dfac2  8579  infpssrlem4  8754  hsmexlem2  8875  hsmexlem4  8877  domtriomlem  8890  axdc3lem2  8899  axdc3lem4  8901  axdc4lem  8903  zorn2lem5  8948  konigthlem  9011  eltsk2g  9194  dedekind  9815  dedekindle  9816  lble  10580  fsuppmapnn0fiublem  12240  fsuppmapnn0fiub  12241  fsuppmapnn0fiubex  12242  prodeq2ii  14044  fprodle  14127  lcmfunsnlem1  14689  lcmfunsnlem2lem1  14690  lcmfunsnlem2  14692  mreiincl  15580  mreexexd  15632  catpropd  15692  acsmapd  16502  gsummatr01lem4  19760  cpmatmcllem  19819  pmatcollpwfi  19883  alexsubALTlem3  21142  isucn2  21372  mptelee  25004  chirred  28129  foresf1o  28218  abrexss  28225  aciunf1lem  28339  nn0min  28459  isarchiofld  28654  reff  28740  locfinreflem  28741  cmpcref  28751  esumcl  28925  measvunilem  29108  measvunilem0  29109  measvuni  29110  voliune  29125  volfiniune  29126  omssubadd  29201  omssubaddOLD  29205  bnj1366  29713  bnj1379  29714  bnj571  29789  bnj1039  29852  bnj1128  29871  bnj1204  29893  bnj1279  29899  bnj1307  29904  bnj1388  29914  bnj1398  29915  bnj1444  29924  bnj1489  29937  bnj1525  29950  dfon2lem3  30502  trpredmintr  30543  frrlem4  30588  heicant  32039  cover2  32104  upixp  32120  indexdom  32125  filbcmb  32131  riotasvd  32592  riotasv2d  32593  riotasv2s  32594  glbconxN  33014  pmapglbx  33405  pmapglb2xN  33408  cdleme26ee  33998  cdlemefr29exN  34040  cdlemefs32sn1aw  34052  cdleme43fsv1snlem  34058  cdleme41sn3a  34071  cdleme32d  34082  cdleme32f  34084  cdleme40m  34105  cdleme40n  34106  cdlemk36  34551  cdlemk38  34553  cdlemkid  34574  cdlemk19x  34581  cdlemk11t  34584  mzpexpmpt  35658  ssralv2  36958  tratrb  36967  fnchoice  37413  rfcnnnub  37420  uzwo4  37451  ralimralim  37488  suprnmpt  37512  fompt  37538  choicefi  37552  upbdrech  37611  ssfiunibd  37615  iuneqfzuzlem  37644  infxrunb2  37678  infrglbOLD  37766  mccl  37775  climsuse  37784  mullimc  37793  islptre  37796  mullimcf  37800  limcrecl  37806  islpcn  37816  limsupre  37818  limsupreOLD  37819  limcleqr  37822  addlimc  37826  0ellimcdiv  37827  limclner  37829  cncfioobd  37872  stoweidlem16  37988  stoweidlem28  38000  stoweidlem29  38001  stoweidlem29OLD  38002  stoweidlem31  38004  stoweidlem35  38008  stoweidlem48  38021  stoweidlem51  38024  stoweidlem52  38025  stoweidlem53  38026  stoweidlem54  38027  stoweidlem56  38029  stoweidlem57  38030  stoweidlem59  38032  stoweidlem60  38033  stoweidlem62  38035  stoweidlem62OLD  38036  wallispilem3  38041  stirlinglem13  38060  fourierdlem31  38112  fourierdlem31OLD  38113  fourierdlem39  38121  fourierdlem68  38150  fourierdlem71  38153  fourierdlem73  38155  fourierdlem77  38159  fourierdlem83  38165  fourierdlem87  38169  fourierdlem94  38176  fourierdlem103  38185  fourierdlem104  38186  fourierdlem112  38194  fourierdlem113  38195  salexct  38305  sge0lefi  38354  sge0isum  38383  iundjiun  38414  voliunsge0lem  38426  ovnsubaddlem2  38511  hoiqssbllem3  38564  2reu1  38752  2reu4a  38755  ffnafv  38818  iccelpart  38892  aacllem  41046
  Copyright terms: Public domain W3C validator