Theorem nfcv 2392

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

This proof depends on syntax axioms:   ∈ wcel 2209  Ⅎwnfc 2379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-nfc 2381

This theorem is used by:  nfcvd  2393  nfel  2401  nfeq1  2402  nfel1  2403  nfeq2  2404  nfel2  2405  nfcvf  2415  r2al  2569  r2ex  2570  nfraldxy  2583  nfrexdxy  2584  nfra2xy  2592  r19.12  2657  ralcom  2714  rexcom  2715  nfreudxy  2725  raleq  2749  rexeq  2750  reueq1  2751  rmoeq1  2752  cbvralw  2779  cbvrexw  2780  cbvral  2782  cbvrex  2783  rabeq  2813  rabeqi  2814  cbvrabv  2820  vtoclg  2883  vtocl2g  2887  vtoclga  2889  vtocl2ga  2891  vtocl3ga  2893  spcimdv  2909  spcimedv  2911  spcgv  2912  spcegv  2913  rspct  2922  rspc  2923  rspce  2924  rspc2  2941  ceqsexg  2954  elabgt  2967  elabf  2969  elabg  2972  elab3g  2977  elrab  2982  mob  3008  nfsbc1v  3070  elrabsf  3090  sbcralt  3128  sbcrext  3129  sbcralg  3130  sbcrex  3131  sbcreug  3132  reu8nf  3133  cbvcsbv  3153  csbconstg  3161  nfcsb1v  3180  csbie  3193  csbnestg  3202  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  cbvralv2  3214  cbvrexv2  3215  dfss4st  3464  n0rf  3534  n0r  3535  eq0  3540  raaanlem  3632  nfpw  3705  cbviunv  4051  cbviinv  4052  ssiun2s  4056  iunab  4059  ssiinf  4062  ssiin  4063  iinab  4074  cbvdisjv  4117  nfdisjv  4118  disjnims  4121  disji2  4122  invdisjrab  4124  cbvmptv  4227  triun  4242  csbexga  4261  repizf2  4299  moop2  4392  euotd  4395  opelopabgf  4412  opelopabf  4417  nfpo  4446  nfso  4447  pofun  4457  nfse  4486  nffrfor  4493  nffr  4494  frind  4497  nfwe  4500  eusvnf  4599  rabxfrd  4615  tfis  4730  tfisi  4734  opeliunxp  4830  nfrel  4860  opeliunxp2  4920  ralxpf  4926  rexxpf  4927  nfco  4945  nfcnv  4959  dfdmf  4974  dfrnf  5023  nfdm  5026  nfres  5065  resmptf  5113  nfiotadw  5340  dffun6f  5390  dffun6  5391  dffun4f  5393  nffun  5400  funimaexglem  5464  nffv  5705  nffvmpt1  5706  dffn5imf  5758  funfvdm2f  5768  fvmptss2  5780  fvmpts  5783  fvmpt2  5789  fvmptssdm  5790  mptfvex  5791  fvmptdv  5794  fvmptd3  5799  elfvmptrab1  5801  eqfnfv2f  5810  ralrnmpt  5850  rexrnmpt  5851  f1ompt  5859  ffnfvf  5867  fmptco  5874  fmptcof  5875  fmptcos  5876  dfimafnf  5955  funiunfvdmf  5970  dff13f  5976  f1mpt  5977  fliftfuns  6004  nfiso  6012  nfriotadxy  6047  csbriotag  6052  riota2  6062  mpoeq123  6147  cbvmpox  6166  cbvmpo  6167  cbvmpov  6168  ovmpos  6212  ov2gf  6213  ovmpodxf  6214  ovmpodx  6215  ovmpodv  6221  ovmpodv2  6222  fvmpopr2d  6225  ovi3  6226  elovmporab  6289  elovmporab1w  6290  nfof  6308  nfofr  6309  offval2  6318  ofrfval2  6319  abrexex2g  6349  abrexex2  6353  uchoice  6371  dfopab2  6423  dfoprab3s  6424  mpomptsx  6433  dmmpossx  6435  fmpox  6436  mpofvex  6441  fnmpoovd  6451  fmpoco  6452  dfmpo  6459  f1od2  6471  disjxp1  6472  mpoxopoveq  6511  mpoxopovel  6512  nftpos  6550  tposoprab  6551  nfrecs  6578  nffrec  6667  eqerlem  6838  qliftfuns  6893  cbvixpv  6998  nfixpxy  6999  nfixp1  7000  ixpf  7002  mptelixpg  7016  dom2lem  7058  modom  7108  xpcomco  7124  xpf1o  7144  mapxpen  7148  ac6sfi  7202  opabfi  7247  nfsup  7333  nfdju  7383  exmidomni  7483  ismkvnex  7496  cc2  7634  cc4f  7636  cc4  7637  caucvgprprlemaddq  8076  caucvgsrlemgt1  8163  axpre-suploclemres  8269  lble  9280  supinfneg  10005  infsupneg  10006  fzrevral  10523  zsupcllemstep  10673  infssuzex  10677  infssuzcldc  10679  infssfzcldc  10680  infssfzledc  10681  nfseq  10909  seq3f1olemstep  10966  seq3f1olemp  10967  nfwrd  11349  reuccatpfxs1v  11536  fimaxre2  12010  nfsum1  12141  nfsum  12142  cbvsumv  12146  cbvsumi  12147  sumfct  12159  sumrbdclem  12163  summodclem2a  12167  zsumdc  12170  fsum3  12173  isumss  12177  isumss2  12179  fsum3cvg2  12180  fsumzcl2  12191  fsumadd  12192  fsumsplitf  12194  sumsnf  12195  sumsn  12197  sumsns  12201  fsumsplitsnun  12205  fsum2dlemstep  12220  fisumcom2  12224  fsumshftm  12231  fsum00  12248  fsumrelem  12257  fsumiun  12263  mertenslem2  12322  prodeq1  12339  nfcprod1  12340  nfcprod  12341  cbvprod  12344  cbvprodv  12345  cbvprodi  12346  prodrbdclem  12357  prodmodclem2a  12362  zproddc  12365  fprodseq  12369  fprodntrivap  12370  prodfct  12373  prodssdc  12375  prodsnf  12378  prodsn  12379  fprodm1s  12387  fprodp1s  12388  prodsns  12389  fprodcllemf  12399  fprodconst  12406  fprodap0  12407  fprod2dlemstep  12408  fprodcom2fi  12412  fprodrec  12415  fproddivapf  12417  fprodsplitf  12418  fprodap0f  12422  fprodle  12426  bezoutlemmain  12794  bezout  12807  nnwofdc  12834  nnwosdc  12835  prmind2  12917  nnmaxpwlemdvds  12968  nnmaxpwlemndvds  12969  pcmpt  13145  pcmptdvds  13147  ctiunctlemudc  13380  ctiunctlemf  13381  ctiunctlemfo  13382  ctiunct  13383  ctiunctal  13384  gzsumconstf  14228  gzsumsplit0  14232  gsumsncmn  14240  gsummptfidmadd  14245  prdsbas3  14271  cnmpt11  15475  cnmpt1t  15477  cnmpt21  15483  cnmpt2t  15485  cnmptcom  15490  imasnopn  15491  fsumcncntop  15759  ellimc3apf  15852  ellimc3ap  15853  limcmpted  15855  dvmptfsum  15917  elplyd  15933  fsumdvdsmul  16246  lgseisenlem2  16356  gropd  16454  grstructd2dom  16455  lfgrnloopen  16540  elabf1  16975  elabf2  16976  elabg2  16979  bj-omssind  17127  bj-bdfindisg  17140  bj-nntrans  17143  bj-nnelirr  17145  bj-omtrans  17148  setindis  17159  bdsetindis  17161  bj-nn0sucALT  17170  bj-findis  17171  bj-findisg  17172  strcollnfALT  17178  isomninnlem  17245  trilpolemeq1  17256  trirec0  17260  iswomninnlem  17266  ismkvnnlem  17269  nconstwlpolemgt0  17281