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

Theorem nfra1 2822
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 2796 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 nfa1 1881 . 2  |-  F/ x A. x ( x  e.  A  ->  ph )
31, 2nfxfr 1630 1  |-  F/ x A. x  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1379   F/wnf 1601    e. wcel 1802   A.wral 2791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-12 1838
This theorem depends on definitions:  df-bi 185  df-ex 1598  df-nf 1602  df-ral 2796
This theorem is referenced by:  hbra1  2823  nfra2  2828  r19.12  2967  ralbi  2972  ralcom2  3006  nfss  3479  rspn0  3779  ralidm  3914  nfii1  4342  dfiun2g  4343  mpteq12f  4509  reusv1  4633  reusv2lem1  4634  reusv2lem2  4635  reusv2lem3  4636  reusv6OLD  4644  ralxfrALT  4652  fvmptss  5945  ffnfv  6038  riota5f  6263  mpt2eq123  6337  tfinds  6675  peano5  6704  fun11iun  6741  zfrep6  6749  tfr3  7066  tz7.48-1  7106  tz7.49  7108  nfixp1  7487  nneneq  7698  scottex  8301  dfac2  8509  infpssrlem4  8684  hsmexlem2  8805  hsmexlem4  8807  domtriomlem  8820  axdc3lem2  8829  axdc3lem4  8831  axdc4lem  8833  zorn2lem5  8878  konigthlem  8941  eltsk2g  9127  dedekind  9742  dedekindle  9743  lble  10496  fsuppmapnn0fiublem  12070  fsuppmapnn0fiub  12071  fsuppmapnn0fiubex  12072  mreiincl  14865  mreexexd  14917  catpropd  14976  acsmapd  15677  gsummatr01lem4  19027  cpmatmcllem  19086  pmatcollpwfi  19150  bwthOLD  19777  alexsubALTlem3  20415  isucn2  20648  mptelee  24063  chirred  27179  foresf1o  27268  abrexss  27275  nn0min  27477  isarchiofld  27673  reff  27708  locfinreflem  27709  cmpcref  27719  esumcl  27909  measvunilem  28049  measvunilem0  28050  measvuni  28051  voliune  28067  volfiniune  28068  prodeq2ii  29013  dfon2lem3  29185  trpredmintr  29282  wfrlem4  29314  frrlem4  29358  heicant  30017  cover2  30172  upixp  30188  indexdom  30193  filbcmb  30199  mzpexpmpt  30645  fnchoice  31351  rfcnnnub  31358  suprnmpt  31397  upbdrech  31450  ssfiunibd  31454  infrglb  31508  climsuse  31518  mullimc  31526  islptre  31529  mullimcf  31533  limcrecl  31539  islpcn  31549  limsupre  31551  limcleqr  31554  addlimc  31558  0ellimcdiv  31559  limclner  31561  cncfioobd  31603  stoweidlem16  31683  stoweidlem28  31695  stoweidlem29  31696  stoweidlem31  31698  stoweidlem35  31702  stoweidlem48  31715  stoweidlem51  31718  stoweidlem52  31719  stoweidlem53  31720  stoweidlem54  31721  stoweidlem56  31723  stoweidlem57  31724  stoweidlem59  31726  stoweidlem60  31727  stoweidlem62  31729  wallispilem3  31734  stirlinglem13  31753  fourierdlem31  31805  fourierdlem39  31813  fourierdlem68  31842  fourierdlem71  31845  fourierdlem73  31847  fourierdlem77  31851  fourierdlem83  31857  fourierdlem87  31861  fourierdlem94  31868  fourierdlem103  31877  fourierdlem104  31878  fourierdlem112  31886  fourierdlem113  31887  2reu1  32025  2reu4a  32028  ffnafv  32090  ssralv2  33009  tratrb  33015  bnj1366  33595  bnj1379  33596  bnj571  33671  bnj1039  33734  bnj1128  33753  bnj1204  33775  bnj1279  33781  bnj1307  33786  bnj1388  33796  bnj1398  33797  bnj1444  33806  bnj1489  33819  bnj1525  33832  riotasvd  34389  riotasv2d  34390  riotasv2s  34391  glbconxN  34804  pmapglbx  35195  pmapglb2xN  35198  cdleme26ee  35788  cdlemefr29exN  35830  cdlemefs32sn1aw  35842  cdleme43fsv1snlem  35848  cdleme41sn3a  35861  cdleme32d  35872  cdleme32f  35874  cdleme40m  35895  cdleme40n  35896  cdlemk36  36341  cdlemk38  36343  cdlemkid  36364  cdlemk19x  36371  cdlemk11t  36374
  Copyright terms: Public domain W3C validator