Theorem nfcv 2384

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

Syntax hints:   ∈ wcel 2203  Ⅎwnfc 2371

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 1498  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-nfc 2373

This theorem is referenced by:  nfcvd  2385  nfel  2393  nfeq1  2394  nfel1  2395  nfeq2  2396  nfel2  2397  nfcvf  2407  r2al  2561  r2ex  2562  nfraldxy  2575  nfrexdxy  2576  nfra2xy  2584  r19.12  2649  ralcom  2706  rexcom  2707  nfreudxy  2717  raleq  2740  rexeq  2741  reueq1  2742  rmoeq1  2743  cbvralw  2770  cbvrexw  2771  cbvral  2773  cbvrex  2774  rabeq  2804  rabeqi  2805  cbvrabv  2811  vtoclg  2874  vtocl2g  2878  vtoclga  2880  vtocl2ga  2882  vtocl3ga  2884  spcimdv  2900  spcimedv  2902  spcgv  2903  spcegv  2904  rspct  2913  rspc  2914  rspce  2915  rspc2  2931  ceqsexg  2944  elabgt  2957  elabf  2959  elabg  2962  elab3g  2967  elrab  2972  mob  2998  nfsbc1v  3060  elrabsf  3080  sbcralt  3118  sbcrext  3119  sbcralg  3120  sbcrex  3121  sbcreug  3122  reu8nf  3123  cbvcsbv  3143  csbconstg  3151  nfcsb1v  3170  csbie  3183  csbnestg  3192  cbvralcsf  3200  cbvrexcsf  3201  cbvreucsf  3202  cbvrabcsf  3203  cbvralv2  3204  cbvrexv2  3205  dfss4st  3453  n0rf  3520  n0r  3521  eq0  3526  raaanlem  3613  nfpw  3684  cbviunv  4029  cbviinv  4030  ssiun2s  4034  iunab  4037  ssiinf  4040  ssiin  4041  iinab  4052  cbvdisjv  4095  nfdisjv  4096  disjnims  4099  disji2  4100  invdisjrab  4102  cbvmptv  4205  triun  4220  csbexga  4237  repizf2  4274  moop2  4367  euotd  4370  opelopabgf  4387  opelopabf  4392  nfpo  4421  nfso  4422  pofun  4432  nfse  4461  nffrfor  4468  nffr  4469  frind  4472  nfwe  4475  eusvnf  4573  rabxfrd  4589  tfis  4704  tfisi  4708  opeliunxp  4804  nfrel  4834  opeliunxp2  4894  ralxpf  4900  rexxpf  4901  nfco  4919  nfcnv  4933  dfdmf  4948  dfrnf  4997  nfdm  5000  nfres  5039  resmptf  5087  nfiotadw  5314  dffun6f  5364  dffun6  5365  dffun4f  5367  nffun  5374  funimaexglem  5438  nffv  5679  nffvmpt1  5680  dffn5imf  5731  funfvdm2f  5741  fvmptss2  5751  fvmpts  5754  fvmpt2  5760  fvmptssdm  5761  mptfvex  5762  fvmptdv  5765  fvmptd3  5770  elfvmptrab1  5771  eqfnfv2f  5778  ralrnmpt  5818  rexrnmpt  5819  f1ompt  5827  ffnfvf  5835  fmptco  5842  fmptcof  5843  fmptcos  5844  funiunfvdmf  5936  dff13f  5942  f1mpt  5943  fliftfuns  5970  nfiso  5978  nfriotadxy  6011  csbriotag  6016  riota2  6026  mpoeq123  6111  cbvmpox  6130  cbvmpo  6131  cbvmpov  6132  ovmpos  6176  ov2gf  6177  ovmpodxf  6178  ovmpodx  6179  ovmpodv  6185  ovmpodv2  6186  fvmpopr2d  6189  ovi3  6190  elovmporab  6253  elovmporab1w  6254  nfof  6271  nfofr  6272  offval2  6281  ofrfval2  6282  abrexex2g  6312  abrexex2  6316  uchoice  6330  dfopab2  6382  dfoprab3s  6383  mpomptsx  6392  dmmpossx  6394  fmpox  6395  mpofvex  6400  fnmpoovd  6410  fmpoco  6411  dfmpo  6418  f1od2  6430  disjxp1  6431  mpoxopoveq  6470  mpoxopovel  6471  nftpos  6509  tposoprab  6510  nfrecs  6537  nffrec  6626  eqerlem  6797  qliftfuns  6852  cbvixpv  6950  nfixpxy  6951  nfixp1  6952  ixpf  6954  mptelixpg  6968  dom2lem  7010  modom  7060  xpcomco  7076  xpf1o  7096  mapxpen  7100  ac6sfi  7154  opabfi  7199  nfsup  7282  nfdju  7332  exmidomni  7432  ismkvnex  7445  cc2  7580  cc4f  7582  cc4  7583  caucvgprprlemaddq  8022  caucvgsrlemgt1  8109  axpre-suploclemres  8215  lble  9220  supinfneg  9926  infsupneg  9927  fzrevral  10438  zsupcllemstep  10588  infssuzex  10592  infssuzcldc  10594  nfseq  10818  seq3f1olemstep  10875  seq3f1olemp  10876  nfwrd  11249  reuccatpfxs1v  11436  fimaxre2  11908  nfsum1  12037  nfsum  12038  cbvsumv  12042  cbvsumi  12043  sumfct  12055  sumrbdclem  12059  summodclem2a  12063  zsumdc  12066  fsum3  12069  isumss  12073  isumss2  12075  fsum3cvg2  12076  fsumzcl2  12087  fsumadd  12088  fsumsplitf  12090  sumsnf  12091  sumsn  12093  sumsns  12097  fsumsplitsnun  12101  fsum2dlemstep  12116  fisumcom2  12120  fsumshftm  12127  fsum00  12144  fsumrelem  12153  fsumiun  12159  mertenslem2  12218  prodeq1  12235  nfcprod1  12236  nfcprod  12237  cbvprod  12240  cbvprodv  12241  cbvprodi  12242  prodrbdclem  12253  prodmodclem2a  12258  zproddc  12261  fprodseq  12265  fprodntrivap  12266  prodfct  12269  prodssdc  12271  prodsnf  12274  prodsn  12275  fprodm1s  12283  fprodp1s  12284  prodsns  12285  fprodcllemf  12295  fprodconst  12302  fprodap0  12303  fprod2dlemstep  12304  fprodcom2fi  12308  fprodrec  12311  fproddivapf  12313  fprodsplitf  12314  fprodap0f  12318  fprodle  12322  bezoutlemmain  12690  bezout  12703  nnwofdc  12730  nnwosdc  12731  prmind2  12813  oddpwdclemdvds  12863  oddpwdclemndvds  12864  pcmpt  13037  pcmptdvds  13039  ctiunctlemudc  13180  ctiunctlemf  13181  ctiunctlemfo  13182  ctiunct  13183  ctiunctal  13184  prdsbas3  13492  gsumfzconstf  14051  gsumsplit0  14055  cnmpt11  15140  cnmpt1t  15142  cnmpt21  15148  cnmpt2t  15150  cnmptcom  15155  imasnopn  15156  fsumcncntop  15424  ellimc3apf  15517  ellimc3ap  15518  limcmpted  15520  dvmptfsum  15582  elplyd  15598  fsumdvdsmul  15851  lgseisenlem2  15936  gropd  16034  grstructd2dom  16035  lfgrnloopen  16120  elabf1  16545  elabf2  16546  elabg2  16549  bj-omssind  16697  bj-bdfindisg  16710  bj-nntrans  16713  bj-nnelirr  16715  bj-omtrans  16718  setindis  16729  bdsetindis  16731  bj-nn0sucALT  16740  bj-findis  16741  bj-findisg  16742  strcollnfALT  16748  isomninnlem  16806  trilpolemeq1  16816  trirec0  16820  iswomninnlem  16826  ismkvnnlem  16829  nconstwlpolemgt0  16841  gfsumsn  16858