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

Theorem nfra1 2845
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 2819 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 nfa1 1845 . 2  |-  F/ x A. x ( x  e.  A  ->  ph )
31, 2nfxfr 1625 1  |-  F/ x A. x  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1377   F/wnf 1599    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-ex 1597  df-nf 1600  df-ral 2819
This theorem is referenced by:  hbra1  2846  nfra2  2851  r19.12  2988  ralbi  2993  ralcom2  3026  nfss  3497  rspn0  3797  ralidm  3931  nfii1  4356  dfiun2g  4357  mpteq12f  4523  reusv1  4647  reusv2lem1  4648  reusv2lem2  4649  reusv2lem3  4650  reusv6OLD  4658  ralxfrALT  4666  fvmptss  5956  ffnfv  6045  riota5f  6268  mpt2eq123  6338  tfinds  6672  peano5  6701  fun11iun  6741  zfrep6  6749  tfr3  7065  tz7.48-1  7105  tz7.49  7107  nfixp1  7486  nneneq  7697  scottex  8299  dfac2  8507  infpssrlem4  8682  hsmexlem2  8803  hsmexlem4  8805  domtriomlem  8818  axdc3lem2  8827  axdc3lem4  8829  axdc4lem  8831  zorn2lem5  8876  konigthlem  8939  eltsk2g  9125  dedekind  9739  dedekindle  9740  lble  10491  fsuppmapnn0fiublem  12060  fsuppmapnn0fiub  12061  fsuppmapnn0fiubex  12062  mreiincl  14847  mreexexd  14899  catpropd  14961  acsmapd  15661  gsummatr01lem4  18927  cpmatmcllem  18986  pmatcollpwfi  19050  bwthOLD  19677  alexsubALTlem3  20284  isucn2  20517  mptelee  23874  chirred  26990  abrexss  27084  nn0min  27279  isarchiofld  27470  ordtconlem1  27542  esumcl  27683  measvunilem  27823  measvunilem0  27824  measvuni  27825  voliune  27841  volfiniune  27842  prodeq2ii  28622  dfon2lem3  28794  trpredmintr  28891  wfrlem4  28923  frrlem4  28967  heicant  29626  cover2  29807  upixp  29823  indexdom  29828  filbcmb  29834  mzpexpmpt  30281  fnchoice  30982  rfcnnnub  30989  suprnmpt  31029  upbdrech  31082  ssfiunibd  31086  infrglb  31140  climsuse  31150  mullimc  31158  islptre  31161  mullimcf  31165  limcrecl  31171  islpcn  31181  limsupre  31183  limcleqr  31186  addlimc  31190  0ellimcdiv  31191  limclner  31193  cncfioobd  31236  stoweidlem16  31316  stoweidlem28  31328  stoweidlem29  31329  stoweidlem31  31331  stoweidlem35  31335  stoweidlem48  31348  stoweidlem51  31351  stoweidlem52  31352  stoweidlem53  31353  stoweidlem54  31354  stoweidlem56  31356  stoweidlem57  31357  stoweidlem59  31359  stoweidlem60  31360  stoweidlem62  31362  wallispilem3  31367  stirlinglem13  31386  fourierdlem31  31438  fourierdlem39  31446  fourierdlem68  31475  fourierdlem71  31478  fourierdlem73  31480  fourierdlem77  31484  fourierdlem83  31490  fourierdlem87  31494  fourierdlem94  31501  fourierdlem103  31510  fourierdlem104  31511  fourierdlem112  31519  fourierdlem113  31520  2reu1  31658  2reu4a  31661  ffnafv  31723  ssralv2  32380  tratrb  32386  bnj1366  32967  bnj1379  32968  bnj571  33043  bnj1039  33106  bnj1128  33125  bnj1204  33147  bnj1279  33153  bnj1307  33158  bnj1388  33168  bnj1398  33169  bnj1444  33178  bnj1489  33191  bnj1525  33204  riotasvd  33759  riotasv2d  33760  riotasv2s  33761  glbconxN  34174  pmapglbx  34565  pmapglb2xN  34568  cdleme26ee  35156  cdlemefr29exN  35198  cdlemefs32sn1aw  35210  cdleme43fsv1snlem  35216  cdleme41sn3a  35229  cdleme32d  35240  cdleme32f  35242  cdleme40m  35263  cdleme40n  35264  cdlemk36  35709  cdlemk38  35711  cdlemkid  35732  cdlemk19x  35739  cdlemk11t  35742
  Copyright terms: Public domain W3C validator