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

Theorem nfra1 3223
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 3147 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 nfa1 2148 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1846 1 𝑥𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1528  wnf 1777  wcel 2107  wral 3142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-10 2138
This theorem depends on definitions:  df-bi 208  df-or 844  df-ex 1774  df-nf 1778  df-ral 3147
This theorem is referenced by:  hbra1  3224  nfra2w  3231  nfra2  3232  ralbiOLD  3237  ralrexbidOLD  3327  r19.12  3328  r19.12OLD  3331  ralcom2w  3367  ralcom2  3368  2reu1  3884  nfss  3963  rspn0  4316  ralidm  4457  2reu4lem  4467  nfii1  4950  dfiun2g  4951  dfiun2gOLD  4952  mpteq12f  5145  reusv1  5293  reusv2lem1  5294  reusv2lem2  5295  reusv2lem3  5296  ralxfrALT  5311  fvmptss  6775  ffnfv  6877  riota5f  7137  mpoeq123  7221  tfinds  7565  peano5  7596  fiun  7638  zfrep6  7650  wfrlem4  7952  tfr3  8029  tz7.48-1  8073  tz7.49  8075  nfixp1  8474  nneneq  8692  scottex  9306  dfac2b  9548  infpssrlem4  9720  hsmexlem2  9841  hsmexlem4  9843  domtriomlem  9856  axdc3lem2  9865  axdc3lem4  9867  axdc4lem  9869  zorn2lem5  9914  konigthlem  9982  eltsk2g  10165  dedekind  10795  dedekindle  10796  lble  11585  fsuppmapnn0fiublem  13351  fsuppmapnn0fiub  13352  fsuppmapnn0fiubex  13353  prodeq2ii  15259  fprodle  15342  lcmfunsnlem1  15973  lcmfunsnlem2lem1  15974  lcmfunsnlem2  15976  mreiincl  16859  mreexexd  16911  catpropd  16971  acsmapd  17780  gsummatr01lem4  21183  cpmatmcllem  21242  alexsubALTlem3  22573  isucn2  22803  mptelee  26595  chirred  30086  opreu2reuALT  30154  foresf1o  30179  abrexss  30186  aciunf1lem  30322  nn0min  30450  fprodex01  30455  isarchiofld  30804  reff  30989  locfinreflem  30990  cmpcref  31000  esumcl  31175  measvunilem  31357  measvunilem0  31358  measvuni  31359  voliune  31374  volfiniune  31375  omssubadd  31444  bnj1366  31987  bnj1379  31988  bnj571  32064  bnj1039  32127  bnj1128  32146  bnj1204  32168  bnj1279  32174  bnj1307  32179  bnj1388  32189  bnj1398  32190  bnj1444  32199  bnj1489  32212  bnj1525  32225  dfon2lem3  32914  trpredmintr  32954  frrlem4  33010  nosupbnd1  33098  domalom  34554  ralssiun  34557  fvineqsneu  34561  fvineqsneq  34562  heicant  34794  cover2  34857  upixp  34872  indexdom  34877  filbcmb  34883  riotasvd  35959  riotasv2d  35960  riotasv2s  35961  glbconxN  36381  pmapglbx  36772  pmapglb2xN  36775  cdleme26ee  37363  cdlemefr29exN  37405  cdlemefs32sn1aw  37417  cdleme43fsv1snlem  37423  cdleme41sn3a  37436  cdleme32d  37447  cdleme32f  37449  cdleme40m  37470  cdleme40n  37471  cdlemk36  37916  cdlemk38  37918  cdlemkid  37939  cdlemk19x  37946  cdlemk11t  37949  mzpexpmpt  39203  gneispace  40345  mnuprdlem4  40472  ssralv2  40726  tratrb  40731  fnchoice  41147  rfcnnnub  41154  uzwo4  41176  ralimralim  41206  ralimda  41267  suprnmpt  41291  fompt  41314  choicefi  41324  axccdom  41348  axccd  41356  rnmptlb  41375  rnmptbddlem  41376  rnmptbd2lem  41381  rnmptbdlem  41388  upbdrech  41433  ssfiunibd  41437  iuneqfzuzlem  41463  infxrunb2  41497  xrralrecnnle  41514  supxrunb3  41533  supxrleubrnmpt  41540  unb2ltle  41550  rexabslelem  41553  allbutfiinf  41555  suprleubrnmpt  41557  uzub  41566  infxrgelbrnmpt  41591  mccl  41740  climsuse  41750  mullimc  41758  islptre  41761  mullimcf  41765  limcrecl  41771  islpcn  41781  limsupre  41783  limcleqr  41786  addlimc  41790  0ellimcdiv  41791  limclner  41793  climinf2lem  41848  limsupubuz  41855  climinf3  41858  limsupmnflem  41862  limsupmnfuzlem  41868  limsupre3uzlem  41877  climisp  41888  climrescn  41890  climxrrelem  41891  climxrre  41892  xlimmnfv  41976  xlimpnfv  41980  climxlim2lem  41987  cncfioobd  42041  stoweidlem16  42163  stoweidlem28  42175  stoweidlem29  42176  stoweidlem31  42178  stoweidlem35  42182  stoweidlem48  42195  stoweidlem51  42198  stoweidlem52  42199  stoweidlem53  42200  stoweidlem54  42201  stoweidlem56  42203  stoweidlem57  42204  stoweidlem59  42206  stoweidlem60  42207  stoweidlem62  42209  wallispilem3  42214  stirlinglem13  42233  fourierdlem31  42285  fourierdlem39  42293  fourierdlem68  42321  fourierdlem71  42324  fourierdlem73  42326  fourierdlem77  42330  fourierdlem83  42336  fourierdlem87  42340  fourierdlem94  42347  fourierdlem103  42356  fourierdlem104  42357  fourierdlem112  42365  fourierdlem113  42366  salexct  42479  subsaliuncl  42503  sge0lefi  42542  sge0isum  42571  sge0reuzb  42592  iundjiun  42604  voliunsge0lem  42616  meaiuninc3v  42628  ovnsubaddlem2  42715  hoiqssbllem3  42768  vonioo  42826  vonicc  42829  preimageiingt  42860  preimaleiinlt  42861  issmfle  42884  issmfgt  42895  issmfge  42908  smflimlem2  42910  smfsupmpt  42951  smfinflem  42953  smfinfmpt  42955  smfliminflem  42966  ffnafv  43232  iccelpart  43421  sprsymrelfo  43487  mogoldbb  43778  sbgoldbo  43780  iunord  44607  setrec1lem2  44619  aacllem  44730
  Copyright terms: Public domain W3C validator