Theorem nfra1 2941

Description: The setvar 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

Step	Hyp	Ref	Expression
1		df-ral 2917	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		nfa1 2028	. 2 |- F/ x A. x ( x e. A -> ph )
3	1, 2	nfxfr 1779	1 |- F/ x A. x e. A ph

Syntax hints:   -> wi 4   A.wal 1481   F/wnf 1708   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-10 2019

This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1705  df-nf 1710  df-ral 2917

This theorem is referenced by:  hbra1  2942  nfra2  2946  r19.12  3063  ralbi  3068  ralcom2  3104  nfss  3596  rspn0  3934  ralidm  4075  nfii1  4551  dfiun2g  4552  mpteq12f  4731  reusv1  4866  reusv1OLD  4867  reusv2lem1  4868  reusv2lem2  4869  reusv2lem2OLD  4870  reusv2lem3  4871  ralxfrALT  4887  fvmptss  6292  ffnfv  6388  riota5f  6636  mpt2eq123  6714  tfinds  7059  peano5  7089  fun11iun  7126  zfrep6  7134  wfrlem4  7418  tfr3  7495  tz7.48-1  7538  tz7.49  7540  nfixp1  7928  nneneq  8143  scottex  8748  dfac2  8953  infpssrlem4  9128  hsmexlem2  9249  hsmexlem4  9251  domtriomlem  9264  axdc3lem2  9273  axdc3lem4  9275  axdc4lem  9277  zorn2lem5  9322  konigthlem  9390  eltsk2g  9573  dedekind  10200  dedekindle  10201  lble  10975  fsuppmapnn0fiublem  12789  fsuppmapnn0fiub  12790  fsuppmapnn0fiubOLD  12791  fsuppmapnn0fiubex  12792  prodeq2ii  14643  fprodle  14727  lcmfunsnlem1  15350  lcmfunsnlem2lem1  15351  lcmfunsnlem2  15353  mreiincl  16256  mreexexd  16308  mreexexdOLD  16309  catpropd  16369  acsmapd  17178  gsummatr01lem4  20464  cpmatmcllem  20523  pmatcollpwfi  20587  alexsubALTlem3  21853  isucn2  22083  mptelee  25775  chirred  29254  foresf1o  29343  abrexss  29350  aciunf1lem  29462  nn0min  29567  fprodex01  29571  isarchiofld  29817  reff  29906  locfinreflem  29907  cmpcref  29917  esumcl  30092  measvunilem  30275  measvunilem0  30276  measvuni  30277  voliune  30292  volfiniune  30293  omssubadd  30362  bnj1366  30900  bnj1379  30901  bnj571  30976  bnj1039  31039  bnj1128  31058  bnj1204  31080  bnj1279  31086  bnj1307  31091  bnj1388  31101  bnj1398  31102  bnj1444  31111  bnj1489  31124  bnj1525  31137  dfon2lem3  31690  trpredmintr  31731  frrlem4  31783  nosupbnd1  31860  heicant  33444  cover2  33508  upixp  33524  indexdom  33529  filbcmb  33535  riotasvd  34242  riotasv2d  34243  riotasv2s  34244  glbconxN  34664  pmapglbx  35055  pmapglb2xN  35058  cdleme26ee  35648  cdlemefr29exN  35690  cdlemefs32sn1aw  35702  cdleme43fsv1snlem  35708  cdleme41sn3a  35721  cdleme32d  35732  cdleme32f  35734  cdleme40m  35755  cdleme40n  35756  cdlemk36  36201  cdlemk38  36203  cdlemkid  36224  cdlemk19x  36231  cdlemk11t  36234  mzpexpmpt  37308  gneispace  38432  ssralv2  38737  tratrb  38746  fnchoice  39188  rfcnnnub  39195  uzwo4  39221  ralimralim  39253  ralimda  39326  suprnmpt  39355  fompt  39379  choicefi  39392  axccdom  39416  axccd  39429  rnmptlb  39453  rnmptbddlem  39455  rnmptbd2lem  39463  rnmptbdlem  39470  upbdrech  39519  ssfiunibd  39523  iuneqfzuzlem  39550  infxrunb2  39584  xrralrecnnle  39602  supxrunb3  39623  supxrleubrnmpt  39632  unb2ltle  39642  rexabslelem  39645  allbutfiinf  39647  suprleubrnmpt  39649  uzub  39658  infxrgelbrnmpt  39683  mccl  39830  climsuse  39840  mullimc  39848  islptre  39851  mullimcf  39855  limcrecl  39861  islpcn  39871  limsupre  39873  limcleqr  39876  addlimc  39880  0ellimcdiv  39881  limclner  39883  climinf2lem  39938  limsupubuz  39945  climinf3  39948  limsupmnflem  39952  limsupmnfuzlem  39958  limsupre3uzlem  39967  climisp  39978  climrescn  39980  climxrrelem  39981  climxrre  39982  xlimmnfv  40060  xlimpnfv  40064  climxlim2lem  40071  cncfioobd  40110  stoweidlem16  40233  stoweidlem28  40245  stoweidlem29  40246  stoweidlem31  40248  stoweidlem35  40252  stoweidlem48  40265  stoweidlem51  40268  stoweidlem52  40269  stoweidlem53  40270  stoweidlem54  40271  stoweidlem56  40273  stoweidlem57  40274  stoweidlem59  40276  stoweidlem60  40277  stoweidlem62  40279  wallispilem3  40284  stirlinglem13  40303  fourierdlem31  40355  fourierdlem39  40363  fourierdlem68  40391  fourierdlem71  40394  fourierdlem73  40396  fourierdlem77  40400  fourierdlem83  40406  fourierdlem87  40410  fourierdlem94  40417  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  fourierdlem113  40436  salexct  40552  subsaliuncl  40576  sge0lefi  40615  sge0isum  40644  sge0reuzb  40665  iundjiun  40677  voliunsge0lem  40689  ovnsubaddlem2  40785  hoiqssbllem3  40838  vonioo  40896  vonicc  40899  preimageiingt  40930  preimaleiinlt  40931  issmfle  40954  issmfgt  40965  issmfge  40978  smflimlem2  40980  smfsupmpt  41021  smfinflem  41023  smfinfmpt  41025  smfliminflem  41036  2reu1  41186  2reu4a  41189  ffnafv  41251  iccelpart  41369  mogoldbb  41673  sbgoldbo  41675  sprsymrelfo  41747  iunord  42422  setrec1lem2  42435  aacllem  42547