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

Theorem nfra1 2724
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 2679 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 nfa1 1802 . 2  |-  F/ x A. x ( x  e.  A  ->  ph )
31, 2nfxfr 1576 1  |-  F/ x A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1546   F/wnf 1550    e. wcel 1721   A.wral 2674
This theorem is referenced by:  nfra2  2728  r19.12  2787  ralbi  2810  ralcom2  2840  nfss  3309  ralidm  3699  nfii1  4090  dfiun2g  4091  mpteq12f  4253  reusv1  4690  reusv2lem1  4691  reusv2lem2  4692  reusv2lem3  4693  reusv6OLD  4701  ralxfrALT  4709  tfinds  4806  peano5  4835  fun11iun  5662  fvmptss  5780  ffnfv  5861  zfrep6  5935  mpt2eq123  6100  riota5f  6541  riotasvd  6559  riotasvdOLD  6560  riotasv2d  6561  riotasv2dOLD  6562  riotasv2s  6563  riotasv3dOLD  6566  tfrlem1  6603  tfr3  6627  tz7.48-1  6667  tz7.49  6669  nfixp1  7049  nneneq  7257  scottex  7773  dfac2  7975  infpssrlem4  8150  hsmexlem2  8271  hsmexlem4  8273  domtriomlem  8286  axdc3lem2  8295  axdc3lem4  8297  axdc4lem  8299  zorn2lem5  8344  konigthlem  8407  eltsk2g  8590  lble  9924  sumeq2ii  12450  mreiincl  13784  mreexexd  13836  catpropd  13898  acsmapd  14567  alexsubALTlem3  18041  isucn2  18270  chirred  23859  abrexss  23954  esumcl  24388  measvunilem  24527  measvunilem0  24528  measvuni  24529  voliune  24546  volfiniune  24547  dedekind  25148  dedekindle  25149  prodeq2ii  25200  dfon2lem3  25363  trpredmintr  25456  wfrlem4  25481  frrlem4  25506  mptelee  25746  cover2  26313  upixp  26329  indexdom  26334  filbcmb  26340  mzpexpmpt  26700  fnchoice  27575  rfcnnnub  27582  infrglb  27597  climsuse  27609  stoweidlem16  27640  stoweidlem28  27652  stoweidlem29  27653  stoweidlem31  27655  stoweidlem35  27659  stoweidlem48  27672  stoweidlem51  27675  stoweidlem52  27676  stoweidlem53  27677  stoweidlem54  27678  stoweidlem56  27680  stoweidlem57  27681  stoweidlem59  27683  stoweidlem60  27684  stoweidlem62  27686  wallispilem3  27691  stirlinglem13  27710  2reu1  27839  2reu4a  27842  ffnafv  27910  ssralv2  28334  tratrb  28339  bnj1366  28919  bnj1379  28920  bnj571  28995  bnj1039  29058  bnj1128  29077  bnj1204  29099  bnj1279  29105  bnj1307  29110  bnj1388  29120  bnj1398  29121  bnj1444  29130  bnj1489  29143  bnj1525  29156  glbconxN  29872  pmapglbx  30263  pmapglb2xN  30266  cdleme26ee  30854  cdlemefr29exN  30896  cdlemefs32sn1aw  30908  cdleme43fsv1snlem  30914  cdleme41sn3a  30927  cdleme32d  30938  cdleme32f  30940  cdleme40m  30961  cdleme40n  30962  cdlemk36  31407  cdlemk38  31409  cdlemkid  31430  cdlemk19x  31437  cdlemk11t  31440
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551  df-ral 2679
  Copyright terms: Public domain W3C validator