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

Theorem nfra1 2756
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 2710 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 nfa1 1829 . 2  |-  F/ x A. x ( x  e.  A  ->  ph )
31, 2nfxfr 1618 1  |-  F/ x A. x  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1360   F/wnf 1592    e. wcel 1755   A.wral 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-ex 1590  df-nf 1593  df-ral 2710
This theorem is referenced by:  nfra2  2760  r19.12  2820  ralbi  2843  ralcom2  2875  nfss  3337  rspn0  3637  ralidm  3771  nfii1  4189  dfiun2g  4190  mpteq12f  4356  reusv1  4480  reusv2lem1  4481  reusv2lem2  4482  reusv2lem3  4483  reusv6OLD  4491  ralxfrALT  4499  fvmptss  5770  ffnfv  5856  riota5f  6065  mpt2eq123  6134  tfinds  6459  peano5  6488  fun11iun  6526  zfrep6  6534  tfr3  6844  tz7.48-1  6884  tz7.49  6886  nfixp1  7271  nneneq  7482  scottex  8080  dfac2  8288  infpssrlem4  8463  hsmexlem2  8584  hsmexlem4  8586  domtriomlem  8599  axdc3lem2  8608  axdc3lem4  8610  axdc4lem  8612  zorn2lem5  8657  konigthlem  8720  eltsk2g  8905  dedekind  9520  dedekindle  9521  lble  10269  mreiincl  14516  mreexexd  14568  catpropd  14630  acsmapd  15330  gsummatr01lem4  18305  bwthOLD  18855  alexsubALTlem3  19462  isucn2  19695  mptelee  22963  chirred  25621  abrexss  25716  nn0min  25912  isarchiofld  26137  ordtconlem1  26207  esumcl  26339  measvunilem  26479  measvunilem0  26480  measvuni  26481  voliune  26498  volfiniune  26499  prodeq2ii  27272  dfon2lem3  27444  trpredmintr  27541  wfrlem4  27573  frrlem4  27617  heicant  28267  cover2  28448  upixp  28464  indexdom  28469  filbcmb  28475  mzpexpmpt  28923  fnchoice  29593  rfcnnnub  29600  infrglb  29614  climsuse  29624  stoweidlem16  29654  stoweidlem28  29666  stoweidlem29  29667  stoweidlem31  29669  stoweidlem35  29673  stoweidlem48  29686  stoweidlem51  29689  stoweidlem52  29690  stoweidlem53  29691  stoweidlem54  29692  stoweidlem56  29694  stoweidlem57  29695  stoweidlem59  29697  stoweidlem60  29698  stoweidlem62  29700  wallispilem3  29705  stirlinglem13  29724  2reu1  29853  2reu4a  29856  ffnafv  29920  ssralv2  30934  tratrb  30940  bnj1366  31522  bnj1379  31523  bnj571  31598  bnj1039  31661  bnj1128  31680  bnj1204  31702  bnj1279  31708  bnj1307  31713  bnj1388  31723  bnj1398  31724  bnj1444  31733  bnj1489  31746  bnj1525  31759  riotasvd  32177  riotasv2d  32178  riotasv2s  32179  glbconxN  32592  pmapglbx  32983  pmapglb2xN  32986  cdleme26ee  33574  cdlemefr29exN  33616  cdlemefs32sn1aw  33628  cdleme43fsv1snlem  33634  cdleme41sn3a  33647  cdleme32d  33658  cdleme32f  33660  cdleme40m  33681  cdleme40n  33682  cdlemk36  34127  cdlemk38  34129  cdlemkid  34150  cdlemk19x  34157  cdlemk11t  34160
  Copyright terms: Public domain W3C validator