Theorem nfcv 2306

Description: If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfcv	⊢ Ⅎ𝑥𝐴

Distinct variable group:   𝑥,𝐴

Proof of Theorem nfcv

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1515	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
2	1	nfci 2296	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:   ∈ wcel 2135  Ⅎwnfc 2293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1436  ax-17 1513

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-nfc 2295

This theorem is referenced by:  nfcvd  2307  nfel  2315  nfeq1  2316  nfel1  2317  nfeq2  2318  nfel2  2319  nfcvf  2329  r2al  2483  r2ex  2484  nfraldxy  2497  nfrexdxy  2498  nfra2xy  2506  r19.12  2570  ralcom  2627  rexcom  2628  nfreudxy  2637  raleq  2659  rexeq  2660  reueq1  2661  rmoeq1  2662  cbvralw  2684  cbvral  2685  cbvrex  2686  rabeq  2713  rabeqi  2714  cbvrabv  2720  vtoclg  2781  vtocl2g  2785  vtoclga  2787  vtocl2ga  2789  vtocl3ga  2791  spcimdv  2805  spcimedv  2807  spcgv  2808  spcegv  2809  rspct  2818  rspc  2819  rspce  2820  rspc2  2836  ceqsexg  2849  elabgt  2862  elabf  2864  elabg  2867  elab3g  2872  elrab  2877  mob  2903  nfsbc1v  2964  elrabsf  2984  sbcralt  3022  sbcrext  3023  sbcralg  3024  sbcrex  3025  sbcreug  3026  cbvcsbv  3046  csbconstg  3054  nfcsb1v  3073  csbie  3085  csbnestg  3094  cbvralcsf  3102  cbvrexcsf  3103  cbvreucsf  3104  cbvrabcsf  3105  cbvralv2  3106  cbvrexv2  3107  dfss4st  3350  n0rf  3416  n0r  3417  eq0  3422  raaanlem  3509  nfpw  3566  cbviunv  3899  cbviinv  3900  ssiun2s  3904  iunab  3906  ssiinf  3909  ssiin  3910  iinab  3921  cbvdisjv  3964  nfdisjv  3965  disjnims  3968  disji2  3969  cbvmptv  4072  triun  4087  csbexga  4104  repizf2  4135  moop2  4223  euotd  4226  opelopabf  4246  nfpo  4273  nfso  4274  pofun  4284  nfse  4313  nffrfor  4320  nffr  4321  frind  4324  nfwe  4327  eusvnf  4425  rabxfrd  4441  tfis  4554  tfisi  4558  opeliunxp  4653  nfrel  4683  opeliunxp2  4738  ralxpf  4744  rexxpf  4745  nfco  4763  nfcnv  4777  dfdmf  4791  dfrnf  4839  nfdm  4842  nfres  4880  resmptf  4928  nfiotadw  5150  dffun6f  5195  dffun6  5196  dffun4f  5198  nffun  5205  funimaexglem  5265  nffv  5490  nffvmpt1  5491  dffn5imf  5535  funfvdm2f  5545  fvmptss2  5555  fvmpts  5558  fvmpt2  5563  fvmptssdm  5564  mptfvex  5565  fvmptdv  5568  fvmptd3  5573  elfvmptrab1  5574  eqfnfv2f  5581  ralrnmpt  5621  rexrnmpt  5622  f1ompt  5630  ffnfvf  5638  fmptco  5645  fmptcof  5646  fmptcos  5647  funiunfvdmf  5726  dff13f  5732  f1mpt  5733  fliftfuns  5760  nfiso  5768  nfriotadxy  5800  csbriotag  5804  riota2  5814  mpoeq123  5892  cbvmpox  5911  cbvmpo  5912  cbvmpov  5913  ovmpos  5956  ov2gf  5957  ovmpodxf  5958  ovmpodx  5959  ovmpodv  5965  ovmpodv2  5966  ovi3  5969  nfof  6049  nfofr  6050  offval2  6059  ofrfval2  6060  abrexex2g  6080  abrexex2  6084  dfopab2  6149  dfoprab3s  6150  mpomptsx  6157  dmmpossx  6159  fmpox  6160  mpofvex  6163  fnmpoovd  6174  fmpoco  6175  dfmpo  6182  f1od2  6194  disjxp1  6195  mpoxopoveq  6199  mpoxopovel  6200  nftpos  6238  tposoprab  6239  nfrecs  6266  nffrec  6355  eqerlem  6523  qliftfuns  6576  cbvixpv  6673  nfixpxy  6674  nfixp1  6675  ixpf  6677  mptelixpg  6691  dom2lem  6729  xpcomco  6783  xpf1o  6801  mapxpen  6805  ac6sfi  6855  nfsup  6948  nfdju  6998  exmidomni  7097  ismkvnex  7110  cc2  7199  cc4f  7201  cc4  7202  caucvgprprlemaddq  7640  caucvgsrlemgt1  7727  axpre-suploclemres  7833  lble  8833  supinfneg  9524  infsupneg  9525  fzrevral  10030  nfseq  10380  seq3f1olemstep  10426  seq3f1olemp  10427  fimaxre2  11154  nfsum1  11283  nfsum  11284  cbvsumv  11288  cbvsumi  11289  sumfct  11301  sumrbdclem  11304  summodclem2a  11308  zsumdc  11311  fsum3  11314  isumss  11318  isumss2  11320  fsum3cvg2  11321  fsumzcl2  11332  fsumadd  11333  fsumsplitf  11335  sumsnf  11336  sumsn  11338  sumsns  11342  fsumsplitsnun  11346  fsum2dlemstep  11361  fisumcom2  11365  fsumshftm  11372  fsum00  11389  fsumrelem  11398  fsumiun  11404  mertenslem2  11463  prodeq1  11480  nfcprod1  11481  nfcprod  11482  cbvprod  11485  cbvprodv  11486  cbvprodi  11487  prodrbdclem  11498  prodmodclem2a  11503  zproddc  11506  fprodseq  11510  fprodntrivap  11511  prodfct  11514  prodssdc  11516  prodsnf  11519  prodsn  11520  fprodm1s  11528  fprodp1s  11529  prodsns  11530  fprodcllemf  11540  fprodconst  11547  fprodap0  11548  fprod2dlemstep  11549  fprodcom2fi  11553  fprodrec  11556  fproddivapf  11558  fprodsplitf  11559  fprodap0f  11563  fprodle  11567  zsupcllemstep  11863  infssuzex  11867  infssuzcldc  11869  bezoutlemmain  11916  bezout  11929  prmind2  12031  oddpwdclemdvds  12079  oddpwdclemndvds  12080  pcmpt  12250  pcmptdvds  12252  ctiunctlemudc  12307  ctiunctlemf  12308  ctiunctlemfo  12309  ctiunct  12310  ctiunctal  12311  cnmpt11  12824  cnmpt1t  12826  cnmpt21  12832  cnmpt2t  12834  cnmptcom  12839  imasnopn  12840  fsumcncntop  13097  ellimc3apf  13170  ellimc3ap  13171  limcmpted  13173  elabf1  13497  elabf2  13498  elabg2  13501  bj-omssind  13652  bj-bdfindisg  13665  bj-nntrans  13668  bj-nnelirr  13670  bj-omtrans  13673  setindis  13684  bdsetindis  13686  bj-nn0sucALT  13695  bj-findis  13696  bj-findisg  13697  strcollnfALT  13703  isomninnlem  13743  trilpolemeq1  13753  trirec0  13757  iswomninnlem  13762  ismkvnnlem  13765  nconstwlpolemgt0  13776