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

Theorem nfra1 2807
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 2781 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 nfa1 1953 . 2  |-  F/ x A. x ( x  e.  A  ->  ph )
31, 2nfxfr 1693 1  |-  F/ x A. x  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1436   F/wnf 1664    e. wcel 1869   A.wral 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-12 1906
This theorem depends on definitions:  df-bi 189  df-ex 1661  df-nf 1665  df-ral 2781
This theorem is referenced by:  hbra1  2808  nfra2  2813  r19.12  2955  ralbi  2960  ralcom2  2994  nfss  3458  rspn0  3775  ralidm  3902  nfii1  4328  dfiun2g  4329  mpteq12f  4498  reusv1  4622  reusv2lem1  4623  reusv2lem2  4624  reusv2lem3  4625  ralxfrALT  4638  fvmptss  5972  ffnfv  6062  riota5f  6289  mpt2eq123  6362  tfinds  6698  peano5  6728  fun11iun  6765  zfrep6  6773  wfrlem4  7045  tfr3  7123  tz7.48-1  7166  tz7.49  7168  nfixp1  7548  nneneq  7759  scottex  8359  dfac2  8563  infpssrlem4  8738  hsmexlem2  8859  hsmexlem4  8861  domtriomlem  8874  axdc3lem2  8883  axdc3lem4  8885  axdc4lem  8887  zorn2lem5  8932  konigthlem  8995  eltsk2g  9178  dedekind  9799  dedekindle  9800  lble  10560  fsuppmapnn0fiublem  12203  fsuppmapnn0fiub  12204  fsuppmapnn0fiubex  12205  prodeq2ii  13960  fprodle  14043  lcmfunsnlem1  14603  lcmfunsnlem2lem1  14604  lcmfunsnlem2  14606  mreiincl  15495  mreexexd  15547  catpropd  15607  acsmapd  16417  gsummatr01lem4  19675  cpmatmcllem  19734  pmatcollpwfi  19798  alexsubALTlem3  21056  isucn2  21286  mptelee  24917  chirred  28040  foresf1o  28132  abrexss  28139  aciunf1lem  28260  nn0min  28385  isarchiofld  28582  reff  28668  locfinreflem  28669  cmpcref  28679  esumcl  28853  measvunilem  29036  measvunilem0  29037  measvuni  29038  voliune  29054  volfiniune  29055  omssubadd  29130  omssubaddOLD  29134  bnj1366  29643  bnj1379  29644  bnj571  29719  bnj1039  29782  bnj1128  29801  bnj1204  29823  bnj1279  29829  bnj1307  29834  bnj1388  29844  bnj1398  29845  bnj1444  29854  bnj1489  29867  bnj1525  29880  dfon2lem3  30432  trpredmintr  30473  frrlem4  30518  heicant  31895  cover2  31960  upixp  31976  indexdom  31981  filbcmb  31987  riotasvd  32453  riotasv2d  32454  riotasv2s  32455  glbconxN  32868  pmapglbx  33259  pmapglb2xN  33262  cdleme26ee  33852  cdlemefr29exN  33894  cdlemefs32sn1aw  33906  cdleme43fsv1snlem  33912  cdleme41sn3a  33925  cdleme32d  33936  cdleme32f  33938  cdleme40m  33959  cdleme40n  33960  cdlemk36  34405  cdlemk38  34407  cdlemkid  34428  cdlemk19x  34435  cdlemk11t  34438  mzpexpmpt  35512  ssralv2  36752  tratrb  36761  fnchoice  37217  rfcnnnub  37224  uzwo4  37260  suprnmpt  37294  fompt  37323  upbdrech  37371  ssfiunibd  37375  iuneqfzuzlem  37405  infrglbOLD  37495  mccl  37504  climsuse  37513  mullimc  37522  islptre  37525  mullimcf  37529  limcrecl  37535  islpcn  37545  limsupre  37547  limsupreOLD  37548  limcleqr  37551  addlimc  37555  0ellimcdiv  37556  limclner  37558  cncfioobd  37601  stoweidlem16  37702  stoweidlem28  37714  stoweidlem29  37715  stoweidlem29OLD  37716  stoweidlem31  37718  stoweidlem35  37722  stoweidlem48  37735  stoweidlem51  37738  stoweidlem52  37739  stoweidlem53  37740  stoweidlem54  37741  stoweidlem56  37743  stoweidlem57  37744  stoweidlem59  37746  stoweidlem60  37747  stoweidlem62  37749  stoweidlem62OLD  37750  wallispilem3  37755  stirlinglem13  37774  fourierdlem31  37826  fourierdlem31OLD  37827  fourierdlem39  37835  fourierdlem68  37864  fourierdlem71  37867  fourierdlem73  37869  fourierdlem77  37873  fourierdlem83  37879  fourierdlem87  37883  fourierdlem94  37890  fourierdlem103  37899  fourierdlem104  37900  fourierdlem112  37908  fourierdlem113  37909  sge0lefi  38034  sge0isum  38063  iundjiun  38083  ovnsubaddlem2  38174  2reu1  38326  2reu4a  38329  ffnafv  38391  iccelpart  38465  aacllem  39846
  Copyright terms: Public domain W3C validator