Theorem nfra1 2838

Description: is not free in . (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)

Assertion

Ref	Expression
nfra1

Proof of Theorem nfra1

Step	Hyp	Ref	Expression
1		df-ral 2812	. 2
2		nfa1 1897	. 2
3	1, 2	nfxfr 1645	1

Syntax hints:  ->wi 4  A.wal 1393  F/wnf 1616  e.wcel 1818  A.wral 2807

This theorem is referenced by:  hbra1  2839  nfra2  2844  r19.12  2983  ralbi  2988  ralcom2  3022  nfss  3496  rspn0  3797  ralidm  3933  nfii1  4361  dfiun2g  4362  mpteq12f  4528  reusv1  4652  reusv2lem1  4653  reusv2lem2  4654  reusv2lem3  4655  reusv6OLD  4663  ralxfrALT  4671  fvmptss  5964  ffnfv  6057  riota5f  6282  mpt2eq123  6356  tfinds  6694  peano5  6723  fun11iun  6760  zfrep6  6768  tfr3  7087  tz7.48-1  7127  tz7.49  7129  nfixp1  7509  nneneq  7720  scottex  8324  dfac2  8532  infpssrlem4  8707  hsmexlem2  8828  hsmexlem4  8830  domtriomlem  8843  axdc3lem2  8852  axdc3lem4  8854  axdc4lem  8856  zorn2lem5  8901  konigthlem  8964  eltsk2g  9150  dedekind  9765  dedekindle  9766  lble  10520  fsuppmapnn0fiublem  12096  fsuppmapnn0fiub  12097  fsuppmapnn0fiubex  12098  prodeq2ii  13720  mreiincl  14993  mreexexd  15045  catpropd  15104  acsmapd  15808  gsummatr01lem4  19160  cpmatmcllem  19219  pmatcollpwfi  19283  bwthOLD  19911  alexsubALTlem3  20549  isucn2  20782  mptelee  24198  chirred  27314  foresf1o  27403  abrexss  27410  nn0min  27611  isarchiofld  27807  reff  27842  locfinreflem  27843  cmpcref  27853  esumcl  28043  measvunilem  28183  measvunilem0  28184  measvuni  28185  voliune  28201  volfiniune  28202  dfon2lem3  29217  trpredmintr  29314  wfrlem4  29346  frrlem4  29390  heicant  30049  cover2  30204  upixp  30220  indexdom  30225  filbcmb  30231  mzpexpmpt  30677  fnchoice  31404  rfcnnnub  31411  suprnmpt  31451  upbdrech  31505  ssfiunibd  31509  infrglb  31584  fprodle  31604  mccl  31606  climsuse  31614  mullimc  31622  islptre  31625  mullimcf  31629  limcrecl  31635  islpcn  31645  limsupre  31647  limcleqr  31650  addlimc  31654  0ellimcdiv  31655  limclner  31657  cncfioobd  31700  stoweidlem16  31798  stoweidlem28  31810  stoweidlem29  31811  stoweidlem31  31813  stoweidlem35  31817  stoweidlem48  31830  stoweidlem51  31833  stoweidlem52  31834  stoweidlem53  31835  stoweidlem54  31836  stoweidlem56  31838  stoweidlem57  31839  stoweidlem59  31841  stoweidlem60  31842  stoweidlem62  31844  wallispilem3  31849  stirlinglem13  31868  fourierdlem31  31920  fourierdlem39  31928  fourierdlem68  31957  fourierdlem71  31960  fourierdlem73  31962  fourierdlem77  31966  fourierdlem83  31972  fourierdlem87  31976  fourierdlem94  31983  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  fourierdlem113  32002  2reu1  32191  2reu4a  32194  ffnafv  32256  aacllem  33216  ssralv2  33301  tratrb  33307  bnj1366  33888  bnj1379  33889  bnj571  33964  bnj1039  34027  bnj1128  34046  bnj1204  34068  bnj1279  34074  bnj1307  34079  bnj1388  34089  bnj1398  34090  bnj1444  34099  bnj1489  34112  bnj1525  34125  riotasvd  34687  riotasv2d  34688  riotasv2s  34689  glbconxN  35102  pmapglbx  35493  pmapglb2xN  35496  cdleme26ee  36086  cdlemefr29exN  36128  cdlemefs32sn1aw  36140  cdleme43fsv1snlem  36146  cdleme41sn3a  36159  cdleme32d  36170  cdleme32f  36172  cdleme40m  36193  cdleme40n  36194  cdlemk36  36639  cdlemk38  36641  cdlemkid  36662  cdlemk19x  36669  cdlemk11t  36672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617  df-ral 2812