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

Theorem nfra1 2699
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 2654 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 nfa1 1796 . 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 1717   A.wral 2649
This theorem is referenced by:  nfra2  2703  r19.12  2762  ralbi  2785  ralcom2  2815  nfss  3284  ralidm  3674  nfii1  4064  dfiun2g  4065  mpteq12f  4226  reusv1  4663  reusv2lem1  4664  reusv2lem2  4665  reusv2lem3  4666  reusv6OLD  4674  ralxfrALT  4682  tfinds  4779  peano5  4808  fun11iun  5635  fvmptss  5752  ffnfv  5833  zfrep6  5907  mpt2eq123  6072  riota5f  6510  riotasvd  6528  riotasvdOLD  6529  riotasv2d  6530  riotasv2dOLD  6531  riotasv2s  6532  riotasv3dOLD  6535  tfrlem1  6572  tfr3  6596  tz7.48-1  6636  tz7.49  6638  nfixp1  7018  nneneq  7226  scottex  7742  dfac2  7944  infpssrlem4  8119  hsmexlem2  8240  hsmexlem4  8242  domtriomlem  8255  axdc3lem2  8264  axdc3lem4  8266  axdc4lem  8268  zorn2lem5  8313  konigthlem  8376  eltsk2g  8559  lble  9892  sumeq2ii  12414  mreiincl  13748  mreexexd  13800  catpropd  13862  acsmapd  14531  alexsubALTlem3  18001  isucn2  18230  chirred  23746  abrexss  23837  esumcl  24223  measvunilem  24360  measvunilem0  24361  measvuni  24362  voliune  24379  volfiniune  24380  dedekind  24966  dedekindle  24967  prodeq2ii  25018  dfon2lem3  25165  trpredmintr  25258  wfrlem4  25283  frrlem4  25308  mptelee  25548  cover2  26106  upixp  26122  indexdom  26127  filbcmb  26133  mzpexpmpt  26493  fnchoice  27368  rfcnnnub  27375  infrglb  27390  climsuse  27402  stoweidlem16  27433  stoweidlem28  27445  stoweidlem29  27446  stoweidlem31  27448  stoweidlem35  27452  stoweidlem48  27465  stoweidlem51  27468  stoweidlem52  27469  stoweidlem53  27470  stoweidlem54  27471  stoweidlem56  27473  stoweidlem57  27474  stoweidlem59  27476  stoweidlem60  27477  stoweidlem62  27479  wallispilem3  27484  stirlinglem13  27503  2reu1  27632  2reu4a  27635  ffnafv  27704  ssralv2  27958  tratrb  27963  bnj1366  28539  bnj1379  28540  bnj571  28615  bnj1039  28678  bnj1128  28697  bnj1204  28719  bnj1279  28725  bnj1307  28730  bnj1388  28740  bnj1398  28741  bnj1444  28750  bnj1489  28763  bnj1525  28776  glbconxN  29492  pmapglbx  29883  pmapglb2xN  29886  cdleme26ee  30474  cdlemefr29exN  30516  cdlemefs32sn1aw  30528  cdleme43fsv1snlem  30534  cdleme41sn3a  30547  cdleme32d  30558  cdleme32f  30560  cdleme40m  30581  cdleme40n  30582  cdlemk36  31027  cdlemk38  31029  cdlemkid  31050  cdlemk19x  31057  cdlemk11t  31060
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 1661  ax-8 1682  ax-6 1736  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551  df-ral 2654
  Copyright terms: Public domain W3C validator