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

Theorem nfra1 3089
Description: The setvar 𝑥 is not free in 𝑥𝐴𝜑. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)
Assertion
Ref Expression
nfra1 𝑥𝑥𝐴 𝜑

Proof of Theorem nfra1
StepHypRef Expression
1 df-ral 3065 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 nfa1 2183 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1928 1 𝑥𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1628  wnf 1855  wcel 2144  wral 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-10 2173
This theorem depends on definitions:  df-bi 197  df-or 827  df-ex 1852  df-nf 1857  df-ral 3065
This theorem is referenced by:  hbra1  3090  nfra2  3094  r19.12  3210  ralbi  3215  ralcom2  3251  nfss  3743  rspn0  4079  ralidm  4214  nfii1  4683  dfiun2g  4684  mpteq12f  4863  reusv1  4994  reusv1OLD  4995  reusv2lem1  4996  reusv2lem2  4997  reusv2lem2OLD  4998  reusv2lem3  4999  ralxfrALT  5015  fvmptss  6434  ffnfv  6530  riota5f  6778  mpt2eq123  6860  tfinds  7205  peano5  7235  fun11iun  7272  zfrep6  7280  wfrlem4  7569  wfrlem4OLD  7570  tfr3  7647  tz7.48-1  7690  tz7.49  7692  nfixp1  8081  nneneq  8298  scottex  8911  dfac2b  9152  dfac2OLD  9154  infpssrlem4  9329  hsmexlem2  9450  hsmexlem4  9452  domtriomlem  9465  axdc3lem2  9474  axdc3lem4  9476  axdc4lem  9478  zorn2lem5  9523  konigthlem  9591  eltsk2g  9774  dedekind  10401  dedekindle  10402  lble  11176  fsuppmapnn0fiublem  12996  fsuppmapnn0fiub  12997  fsuppmapnn0fiubex  12998  prodeq2ii  14849  fprodle  14932  lcmfunsnlem1  15557  lcmfunsnlem2lem1  15558  lcmfunsnlem2  15560  mreiincl  16463  mreexexd  16515  catpropd  16575  acsmapd  17385  gsummatr01lem4  20682  cpmatmcllem  20742  alexsubALTlem3  22072  isucn2  22302  mptelee  25995  chirred  29588  foresf1o  29675  abrexss  29682  aciunf1lem  29796  nn0min  29901  fprodex01  29905  isarchiofld  30151  reff  30240  locfinreflem  30241  cmpcref  30251  esumcl  30426  measvunilem  30609  measvunilem0  30610  measvuni  30611  voliune  30626  volfiniune  30627  omssubadd  30696  bnj1366  31232  bnj1379  31233  bnj571  31308  bnj1039  31371  bnj1128  31390  bnj1204  31412  bnj1279  31418  bnj1307  31423  bnj1388  31433  bnj1398  31434  bnj1444  31443  bnj1489  31456  bnj1525  31469  dfon2lem3  32020  trpredmintr  32061  frrlem4  32114  nosupbnd1  32191  heicant  33770  cover2  33833  upixp  33849  indexdom  33854  filbcmb  33860  riotasvd  34757  riotasv2d  34758  riotasv2s  34759  glbconxN  35179  pmapglbx  35570  pmapglb2xN  35573  cdleme26ee  36162  cdlemefr29exN  36204  cdlemefs32sn1aw  36216  cdleme43fsv1snlem  36222  cdleme41sn3a  36235  cdleme32d  36246  cdleme32f  36248  cdleme40m  36269  cdleme40n  36270  cdlemk36  36715  cdlemk38  36717  cdlemkid  36738  cdlemk19x  36745  cdlemk11t  36748  mzpexpmpt  37827  gneispace  38951  ssralv2  39256  tratrb  39265  fnchoice  39704  rfcnnnub  39711  uzwo4  39736  ralimralim  39768  ralimda  39841  suprnmpt  39869  fompt  39893  choicefi  39904  axccdom  39928  axccd  39941  rnmptlb  39965  rnmptbddlem  39967  rnmptbd2lem  39975  rnmptbdlem  39982  upbdrech  40030  ssfiunibd  40034  iuneqfzuzlem  40060  infxrunb2  40094  xrralrecnnle  40112  supxrunb3  40133  supxrleubrnmpt  40142  unb2ltle  40152  rexabslelem  40155  allbutfiinf  40157  suprleubrnmpt  40159  uzub  40168  infxrgelbrnmpt  40193  mccl  40342  climsuse  40352  mullimc  40360  islptre  40363  mullimcf  40367  limcrecl  40373  islpcn  40383  limsupre  40385  limcleqr  40388  addlimc  40392  0ellimcdiv  40393  limclner  40395  climinf2lem  40450  limsupubuz  40457  climinf3  40460  limsupmnflem  40464  limsupmnfuzlem  40470  limsupre3uzlem  40479  climisp  40490  climrescn  40492  climxrrelem  40493  climxrre  40494  xlimmnfv  40572  xlimpnfv  40576  climxlim2lem  40583  cncfioobd  40622  stoweidlem16  40744  stoweidlem28  40756  stoweidlem29  40757  stoweidlem31  40759  stoweidlem35  40763  stoweidlem48  40776  stoweidlem51  40779  stoweidlem52  40780  stoweidlem53  40781  stoweidlem54  40782  stoweidlem56  40784  stoweidlem57  40785  stoweidlem59  40787  stoweidlem60  40788  stoweidlem62  40790  wallispilem3  40795  stirlinglem13  40814  fourierdlem31  40866  fourierdlem39  40874  fourierdlem68  40902  fourierdlem71  40905  fourierdlem73  40907  fourierdlem77  40911  fourierdlem83  40917  fourierdlem87  40921  fourierdlem94  40928  fourierdlem103  40937  fourierdlem104  40938  fourierdlem112  40946  fourierdlem113  40947  salexct  41063  subsaliuncl  41087  sge0lefi  41126  sge0isum  41155  sge0reuzb  41176  iundjiun  41188  voliunsge0lem  41200  meaiuninc3v  41212  ovnsubaddlem2  41299  hoiqssbllem3  41352  vonioo  41410  vonicc  41413  preimageiingt  41444  preimaleiinlt  41445  issmfle  41468  issmfgt  41479  issmfge  41492  smflimlem2  41494  smfsupmpt  41535  smfinflem  41537  smfinfmpt  41539  smfliminflem  41550  2reu1  41700  2reu4a  41703  ffnafv  41765  iccelpart  41887  mogoldbb  42191  sbgoldbo  42193  sprsymrelfo  42265  iunord  42940  setrec1lem2  42953  aacllem  43068
  Copyright terms: Public domain W3C validator