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

Theorem nfra1 2769
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 2742 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 nfa1 1979 . 2  |-  F/ x A. x ( x  e.  A  ->  ph )
31, 2nfxfr 1696 1  |-  F/ x A. x  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1442   F/wnf 1667    e. wcel 1887   A.wral 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-12 1933
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668  df-ral 2742
This theorem is referenced by:  hbra1  2770  nfra2  2775  r19.12  2916  ralbi  2921  ralcom2  2955  nfss  3425  rspn0  3744  ralidm  3873  nfii1  4309  dfiun2g  4310  mpteq12f  4479  reusv1  4603  reusv2lem1  4604  reusv2lem2  4605  reusv2lem3  4606  ralxfrALT  4619  fvmptss  5958  ffnfv  6049  riota5f  6276  mpt2eq123  6350  tfinds  6686  peano5  6716  fun11iun  6753  zfrep6  6761  wfrlem4  7039  tfr3  7117  tz7.48-1  7160  tz7.49  7162  nfixp1  7542  nneneq  7755  scottex  8356  dfac2  8561  infpssrlem4  8736  hsmexlem2  8857  hsmexlem4  8859  domtriomlem  8872  axdc3lem2  8881  axdc3lem4  8883  axdc4lem  8885  zorn2lem5  8930  konigthlem  8993  eltsk2g  9176  dedekind  9797  dedekindle  9798  lble  10558  fsuppmapnn0fiublem  12202  fsuppmapnn0fiub  12203  fsuppmapnn0fiubex  12204  prodeq2ii  13967  fprodle  14050  lcmfunsnlem1  14610  lcmfunsnlem2lem1  14611  lcmfunsnlem2  14613  mreiincl  15502  mreexexd  15554  catpropd  15614  acsmapd  16424  gsummatr01lem4  19683  cpmatmcllem  19742  pmatcollpwfi  19806  alexsubALTlem3  21064  isucn2  21294  mptelee  24925  chirred  28048  foresf1o  28139  abrexss  28146  aciunf1lem  28264  nn0min  28384  isarchiofld  28580  reff  28666  locfinreflem  28667  cmpcref  28677  esumcl  28851  measvunilem  29034  measvunilem0  29035  measvuni  29036  voliune  29052  volfiniune  29053  omssubadd  29128  omssubaddOLD  29132  bnj1366  29641  bnj1379  29642  bnj571  29717  bnj1039  29780  bnj1128  29799  bnj1204  29821  bnj1279  29827  bnj1307  29832  bnj1388  29842  bnj1398  29843  bnj1444  29852  bnj1489  29865  bnj1525  29878  dfon2lem3  30431  trpredmintr  30472  frrlem4  30517  heicant  31975  cover2  32040  upixp  32056  indexdom  32061  filbcmb  32067  riotasvd  32528  riotasv2d  32529  riotasv2s  32530  glbconxN  32943  pmapglbx  33334  pmapglb2xN  33337  cdleme26ee  33927  cdlemefr29exN  33969  cdlemefs32sn1aw  33981  cdleme43fsv1snlem  33987  cdleme41sn3a  34000  cdleme32d  34011  cdleme32f  34013  cdleme40m  34034  cdleme40n  34035  cdlemk36  34480  cdlemk38  34482  cdlemkid  34503  cdlemk19x  34510  cdlemk11t  34513  mzpexpmpt  35587  ssralv2  36888  tratrb  36897  fnchoice  37350  rfcnnnub  37357  uzwo4  37392  suprnmpt  37439  fompt  37467  choicefi  37481  upbdrech  37523  ssfiunibd  37527  iuneqfzuzlem  37557  infrglbOLD  37669  mccl  37678  climsuse  37687  mullimc  37696  islptre  37699  mullimcf  37703  limcrecl  37709  islpcn  37719  limsupre  37721  limsupreOLD  37722  limcleqr  37725  addlimc  37729  0ellimcdiv  37730  limclner  37732  cncfioobd  37775  stoweidlem16  37876  stoweidlem28  37888  stoweidlem29  37889  stoweidlem29OLD  37890  stoweidlem31  37892  stoweidlem35  37896  stoweidlem48  37909  stoweidlem51  37912  stoweidlem52  37913  stoweidlem53  37914  stoweidlem54  37915  stoweidlem56  37917  stoweidlem57  37918  stoweidlem59  37920  stoweidlem60  37921  stoweidlem62  37923  stoweidlem62OLD  37924  wallispilem3  37929  stirlinglem13  37948  fourierdlem31  38000  fourierdlem31OLD  38001  fourierdlem39  38009  fourierdlem68  38038  fourierdlem71  38041  fourierdlem73  38043  fourierdlem77  38047  fourierdlem83  38053  fourierdlem87  38057  fourierdlem94  38064  fourierdlem103  38073  fourierdlem104  38074  fourierdlem112  38082  fourierdlem113  38083  salexct  38193  sge0lefi  38240  sge0isum  38269  iundjiun  38298  ovnsubaddlem2  38393  hoiqssbllem3  38446  2reu1  38607  2reu4a  38610  ffnafv  38673  iccelpart  38747  aacllem  40593
  Copyright terms: Public domain W3C validator