Theorem nfcv 2332

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 1539	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
2	1	nfci 2322	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:   ∈ wcel 2160  Ⅎwnfc 2319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1460  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-nfc 2321

This theorem is referenced by:  nfcvd  2333  nfel  2341  nfeq1  2342  nfel1  2343  nfeq2  2344  nfel2  2345  nfcvf  2355  r2al  2509  r2ex  2510  nfraldxy  2523  nfrexdxy  2524  nfra2xy  2532  r19.12  2596  ralcom  2653  rexcom  2654  nfreudxy  2664  raleq  2686  rexeq  2687  reueq1  2688  rmoeq1  2689  cbvralw  2712  cbvrexw  2713  cbvral  2714  cbvrex  2715  rabeq  2744  rabeqi  2745  cbvrabv  2751  vtoclg  2812  vtocl2g  2816  vtoclga  2818  vtocl2ga  2820  vtocl3ga  2822  spcimdv  2836  spcimedv  2838  spcgv  2839  spcegv  2840  rspct  2849  rspc  2850  rspce  2851  rspc2  2867  ceqsexg  2880  elabgt  2893  elabf  2895  elabg  2898  elab3g  2903  elrab  2908  mob  2934  nfsbc1v  2996  elrabsf  3016  sbcralt  3054  sbcrext  3055  sbcralg  3056  sbcrex  3057  sbcreug  3058  cbvcsbv  3078  csbconstg  3086  nfcsb1v  3105  csbie  3117  csbnestg  3126  cbvralcsf  3134  cbvrexcsf  3135  cbvreucsf  3136  cbvrabcsf  3137  cbvralv2  3138  cbvrexv2  3139  dfss4st  3383  n0rf  3450  n0r  3451  eq0  3456  raaanlem  3543  nfpw  3606  cbviunv  3943  cbviinv  3944  ssiun2s  3948  iunab  3951  ssiinf  3954  ssiin  3955  iinab  3966  cbvdisjv  4009  nfdisjv  4010  disjnims  4013  disji2  4014  cbvmptv  4117  triun  4132  csbexga  4149  repizf2  4183  moop2  4272  euotd  4275  opelopabf  4295  nfpo  4322  nfso  4323  pofun  4333  nfse  4362  nffrfor  4369  nffr  4370  frind  4373  nfwe  4376  eusvnf  4474  rabxfrd  4490  tfis  4603  tfisi  4607  opeliunxp  4702  nfrel  4732  opeliunxp2  4788  ralxpf  4794  rexxpf  4795  nfco  4813  nfcnv  4827  dfdmf  4841  dfrnf  4889  nfdm  4892  nfres  4930  resmptf  4978  nfiotadw  5202  dffun6f  5251  dffun6  5252  dffun4f  5254  nffun  5261  funimaexglem  5321  nffv  5547  nffvmpt1  5548  dffn5imf  5595  funfvdm2f  5605  fvmptss2  5615  fvmpts  5618  fvmpt2  5623  fvmptssdm  5624  mptfvex  5625  fvmptdv  5628  fvmptd3  5633  elfvmptrab1  5634  eqfnfv2f  5641  ralrnmpt  5682  rexrnmpt  5683  f1ompt  5691  ffnfvf  5699  fmptco  5706  fmptcof  5707  fmptcos  5708  funiunfvdmf  5789  dff13f  5795  f1mpt  5796  fliftfuns  5823  nfiso  5831  nfriotadxy  5864  csbriotag  5868  riota2  5878  mpoeq123  5959  cbvmpox  5978  cbvmpo  5979  cbvmpov  5980  ovmpos  6024  ov2gf  6025  ovmpodxf  6026  ovmpodx  6027  ovmpodv  6033  ovmpodv2  6034  ovi3  6037  nfof  6116  nfofr  6117  offval2  6126  ofrfval2  6127  abrexex2g  6149  abrexex2  6153  dfopab2  6218  dfoprab3s  6219  mpomptsx  6226  dmmpossx  6228  fmpox  6229  mpofvex  6232  fnmpoovd  6244  fmpoco  6245  dfmpo  6252  f1od2  6264  disjxp1  6265  mpoxopoveq  6269  mpoxopovel  6270  nftpos  6308  tposoprab  6309  nfrecs  6336  nffrec  6425  eqerlem  6594  qliftfuns  6649  cbvixpv  6746  nfixpxy  6747  nfixp1  6748  ixpf  6750  mptelixpg  6764  dom2lem  6802  xpcomco  6856  xpf1o  6876  mapxpen  6880  ac6sfi  6930  nfsup  7025  nfdju  7075  exmidomni  7175  ismkvnex  7188  cc2  7301  cc4f  7303  cc4  7304  caucvgprprlemaddq  7742  caucvgsrlemgt1  7829  axpre-suploclemres  7935  lble  8939  supinfneg  9631  infsupneg  9632  fzrevral  10141  nfseq  10494  seq3f1olemstep  10540  seq3f1olemp  10541  fimaxre2  11276  nfsum1  11405  nfsum  11406  cbvsumv  11410  cbvsumi  11411  sumfct  11423  sumrbdclem  11426  summodclem2a  11430  zsumdc  11433  fsum3  11436  isumss  11440  isumss2  11442  fsum3cvg2  11443  fsumzcl2  11454  fsumadd  11455  fsumsplitf  11457  sumsnf  11458  sumsn  11460  sumsns  11464  fsumsplitsnun  11468  fsum2dlemstep  11483  fisumcom2  11487  fsumshftm  11494  fsum00  11511  fsumrelem  11520  fsumiun  11526  mertenslem2  11585  prodeq1  11602  nfcprod1  11603  nfcprod  11604  cbvprod  11607  cbvprodv  11608  cbvprodi  11609  prodrbdclem  11620  prodmodclem2a  11625  zproddc  11628  fprodseq  11632  fprodntrivap  11633  prodfct  11636  prodssdc  11638  prodsnf  11641  prodsn  11642  fprodm1s  11650  fprodp1s  11651  prodsns  11652  fprodcllemf  11662  fprodconst  11669  fprodap0  11670  fprod2dlemstep  11671  fprodcom2fi  11675  fprodrec  11678  fproddivapf  11680  fprodsplitf  11681  fprodap0f  11685  fprodle  11689  zsupcllemstep  11987  infssuzex  11991  infssuzcldc  11993  bezoutlemmain  12040  bezout  12053  nnwofdc  12080  nnwosdc  12081  prmind2  12163  oddpwdclemdvds  12213  oddpwdclemndvds  12214  pcmpt  12386  pcmptdvds  12388  ctiunctlemudc  12499  ctiunctlemf  12500  ctiunctlemfo  12501  ctiunct  12502  ctiunctal  12503  cnmpt11  14268  cnmpt1t  14270  cnmpt21  14276  cnmpt2t  14278  cnmptcom  14283  imasnopn  14284  fsumcncntop  14541  ellimc3apf  14614  ellimc3ap  14615  limcmpted  14617  lgseisenlem2  14937  elabf1  15019  elabf2  15020  elabg2  15023  bj-omssind  15173  bj-bdfindisg  15186  bj-nntrans  15189  bj-nnelirr  15191  bj-omtrans  15194  setindis  15205  bdsetindis  15207  bj-nn0sucALT  15216  bj-findis  15217  bj-findisg  15218  strcollnfALT  15224  isomninnlem  15266  trilpolemeq1  15276  trirec0  15280  iswomninnlem  15285  ismkvnnlem  15288  nconstwlpolemgt0  15300