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 1806 . 2  |-  F/ x A. x ( x  e.  A  ->  ph )
31, 2nfxfr 1579 1  |-  F/ x A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549   F/wnf 1553    e. wcel 1725   A.wral 2705
This theorem is referenced by:  nfra2  2760  r19.12  2819  ralbi  2842  ralcom2  2872  nfss  3341  ralidm  3731  nfii1  4122  dfiun2g  4123  mpteq12f  4285  reusv1  4723  reusv2lem1  4724  reusv2lem2  4725  reusv2lem3  4726  reusv6OLD  4734  ralxfrALT  4742  tfinds  4839  peano5  4868  fun11iun  5695  fvmptss  5813  ffnfv  5894  zfrep6  5968  mpt2eq123  6133  riota5f  6574  riotasvd  6592  riotasvdOLD  6593  riotasv2d  6594  riotasv2dOLD  6595  riotasv2s  6596  riotasv3dOLD  6599  tfrlem1  6636  tfr3  6660  tz7.48-1  6700  tz7.49  6702  nfixp1  7082  nneneq  7290  scottex  7809  dfac2  8011  infpssrlem4  8186  hsmexlem2  8307  hsmexlem4  8309  domtriomlem  8322  axdc3lem2  8331  axdc3lem4  8333  axdc4lem  8335  zorn2lem5  8380  konigthlem  8443  eltsk2g  8626  lble  9960  sumeq2ii  12487  mreiincl  13821  mreexexd  13873  catpropd  13935  acsmapd  14604  bwth  17473  alexsubALTlem3  18080  isucn2  18309  chirred  23898  abrexss  23993  esumcl  24427  measvunilem  24566  measvunilem0  24567  measvuni  24568  voliune  24585  volfiniune  24586  dedekind  25187  dedekindle  25188  prodeq2ii  25239  dfon2lem3  25412  trpredmintr  25509  wfrlem4  25541  frrlem4  25585  mptelee  25834  cover2  26415  upixp  26431  indexdom  26436  filbcmb  26442  mzpexpmpt  26802  fnchoice  27676  rfcnnnub  27683  infrglb  27698  climsuse  27710  stoweidlem16  27741  stoweidlem28  27753  stoweidlem29  27754  stoweidlem31  27756  stoweidlem35  27760  stoweidlem48  27773  stoweidlem51  27776  stoweidlem52  27777  stoweidlem53  27778  stoweidlem54  27779  stoweidlem56  27781  stoweidlem57  27782  stoweidlem59  27784  stoweidlem60  27785  stoweidlem62  27787  wallispilem3  27792  stirlinglem13  27811  2reu1  27940  2reu4a  27943  ffnafv  28011  ssralv2  28615  tratrb  28620  bnj1366  29201  bnj1379  29202  bnj571  29277  bnj1039  29340  bnj1128  29359  bnj1204  29381  bnj1279  29387  bnj1307  29392  bnj1388  29402  bnj1398  29403  bnj1444  29412  bnj1489  29425  bnj1525  29438  glbconxN  30175  pmapglbx  30566  pmapglb2xN  30569  cdleme26ee  31157  cdlemefr29exN  31199  cdlemefs32sn1aw  31211  cdleme43fsv1snlem  31217  cdleme41sn3a  31230  cdleme32d  31241  cdleme32f  31243  cdleme40m  31264  cdleme40n  31265  cdlemk36  31710  cdlemk38  31712  cdlemkid  31733  cdlemk19x  31740  cdlemk11t  31743
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554  df-ral 2710
  Copyright terms: Public domain W3C validator