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

Theorem nfra1 2835
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 2809 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 nfa1 1902 . 2  |-  F/ x A. x ( x  e.  A  ->  ph )
31, 2nfxfr 1650 1  |-  F/ x A. x  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1396   F/wnf 1621    e. wcel 1823   A.wral 2804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622  df-ral 2809
This theorem is referenced by:  hbra1  2836  nfra2  2841  r19.12  2980  ralbi  2985  ralcom2  3019  nfss  3482  rspn0  3796  ralidm  3921  nfii1  4346  dfiun2g  4347  mpteq12f  4515  reusv1  4637  reusv2lem1  4638  reusv2lem2  4639  reusv2lem3  4640  reusv6OLD  4648  ralxfrALT  4656  fvmptss  5940  ffnfv  6033  riota5f  6256  mpt2eq123  6329  tfinds  6667  peano5  6696  fun11iun  6733  zfrep6  6741  tfr3  7060  tz7.48-1  7100  tz7.49  7102  nfixp1  7482  nneneq  7693  scottex  8294  dfac2  8502  infpssrlem4  8677  hsmexlem2  8798  hsmexlem4  8800  domtriomlem  8813  axdc3lem2  8822  axdc3lem4  8824  axdc4lem  8826  zorn2lem5  8871  konigthlem  8934  eltsk2g  9118  dedekind  9733  dedekindle  9734  lble  10490  fsuppmapnn0fiublem  12078  fsuppmapnn0fiub  12079  fsuppmapnn0fiubex  12080  prodeq2ii  13802  mreiincl  15085  mreexexd  15137  catpropd  15197  acsmapd  16007  gsummatr01lem4  19327  cpmatmcllem  19386  pmatcollpwfi  19450  alexsubALTlem3  20715  isucn2  20948  mptelee  24400  chirred  27512  foresf1o  27602  abrexss  27609  aciunf1lem  27729  nn0min  27845  isarchiofld  28042  reff  28077  locfinreflem  28078  cmpcref  28088  esumcl  28259  measvunilem  28420  measvunilem0  28421  measvuni  28422  voliune  28438  volfiniune  28439  omssubadd  28508  dfon2lem3  29457  trpredmintr  29554  wfrlem4  29586  frrlem4  29630  heicant  30289  cover2  30444  upixp  30460  indexdom  30465  filbcmb  30471  mzpexpmpt  30917  fnchoice  31644  rfcnnnub  31651  suprnmpt  31691  upbdrech  31744  ssfiunibd  31748  infrglb  31823  fprodle  31843  mccl  31845  climsuse  31853  mullimc  31861  islptre  31864  mullimcf  31868  limcrecl  31874  islpcn  31884  limsupre  31886  limcleqr  31889  addlimc  31893  0ellimcdiv  31894  limclner  31896  cncfioobd  31939  stoweidlem16  32037  stoweidlem28  32049  stoweidlem29  32050  stoweidlem31  32052  stoweidlem35  32056  stoweidlem48  32069  stoweidlem51  32072  stoweidlem52  32073  stoweidlem53  32074  stoweidlem54  32075  stoweidlem56  32077  stoweidlem57  32078  stoweidlem59  32080  stoweidlem60  32081  stoweidlem62  32083  wallispilem3  32088  stirlinglem13  32107  fourierdlem31  32159  fourierdlem39  32167  fourierdlem68  32196  fourierdlem71  32199  fourierdlem73  32201  fourierdlem77  32205  fourierdlem83  32211  fourierdlem87  32215  fourierdlem94  32222  fourierdlem103  32231  fourierdlem104  32232  fourierdlem112  32240  fourierdlem113  32241  2reu1  32430  2reu4a  32433  ffnafv  32495  aacllem  33604  ssralv2  33688  tratrb  33697  bnj1366  34289  bnj1379  34290  bnj571  34365  bnj1039  34428  bnj1128  34447  bnj1204  34469  bnj1279  34475  bnj1307  34480  bnj1388  34490  bnj1398  34491  bnj1444  34500  bnj1489  34513  bnj1525  34526  riotasvd  35084  riotasv2d  35085  riotasv2s  35086  glbconxN  35499  pmapglbx  35890  pmapglb2xN  35893  cdleme26ee  36483  cdlemefr29exN  36525  cdlemefs32sn1aw  36537  cdleme43fsv1snlem  36543  cdleme41sn3a  36556  cdleme32d  36567  cdleme32f  36569  cdleme40m  36590  cdleme40n  36591  cdlemk36  37036  cdlemk38  37038  cdlemkid  37059  cdlemk19x  37066  cdlemk11t  37069
  Copyright terms: Public domain W3C validator