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  4229  triun  4244  csbexga  4263  repizf2  4301  moop2  4394  euotd  4397  opelopabgf  4414  opelopabf  4419  nfpo  4448  nfso  4449  pofun  4459  nfse  4488  nffrfor  4495  nffr  4496  frind  4499  nfwe  4502  eusvnf  4601  rabxfrd  4617  tfis  4732  tfisi  4736  opeliunxp  4832  nfrel  4862  opeliunxp2  4922  ralxpf  4928  rexxpf  4929  nfco  4947  nfcnv  4961  dfdmf  4976  dfrnf  5025  nfdm  5028  nfres  5067  resmptf  5116  nfiotadw  5343  dffun6f  5393  dffun6  5394  dffun4f  5396  nffun  5403  funimaexglem  5467  nffv  5708  nffvmpt1  5709  dffn5imf  5761  funfvdm2f  5771  fvmptss2  5783  fvmpts  5786  fvmpt2  5792  fvmptssdm  5793  mptfvex  5794  fvmptdv  5797  fvmptd3  5802  elfvmptrab1  5804  eqfnfv2f  5813  ralrnmpt  5853  rexrnmpt  5854  f1ompt  5862  ffnfvf  5870  fmptco  5877  fmptcof  5878  fmptcos  5879  dfimafnf  5958  funiunfvdmf  5973  dff13f  5979  f1mpt  5980  fliftfuns  6007  nfiso  6015  nfriotadxy  6050  csbriotag  6055  riota2  6065  mpoeq123  6150  cbvmpox  6169  cbvmpo  6170  cbvmpov  6171  ovmpos  6215  ov2gf  6216  ovmpodxf  6217  ovmpodx  6218  ovmpodv  6224  ovmpodv2  6225  fvmpopr2d  6228  ovi3  6229  elovmporab  6292  elovmporab1w  6293  nfof  6312  nfofr  6313  offval2  6322  ofrfval2  6323  abrexex2g  6353  abrexex2  6357  uchoice  6375  dfopab2  6427  dfoprab3s  6428  mpomptsx  6437  dmmpossx  6439  fmpox  6440  mpofvex  6445  fnmpoovd  6455  fmpoco  6456  dfmpo  6463  f1od2  6475  disjxp1  6476  mpoxopoveq  6516  mpoxopovel  6517  nftpos  6555  tposoprab  6556  nfrecs  6583  nffrec  6672  eqerlem  6843  qliftfuns  6898  cbvixpv  7004  nfixpxy  7005  nfixp1  7006  ixpf  7008  mptelixpg  7022  dom2lem  7064  modom  7114  xpcomco  7130  xpf1o  7150  mapxpen  7154  ac6sfi  7208  opabfi  7253  nfsup  7338  nfdju  7388  exmidomni  7488  ismkvnex  7501  cc2  7639  cc4f  7641  cc4  7642  caucvgprprlemaddq  8081  caucvgsrlemgt1  8168  axpre-suploclemres  8274  lble  9285  supinfneg  10010  infsupneg  10011  fzrevral  10528  zsupcllemstep  10678  infssuzex  10682  infssuzcldc  10684  infssfzcldc  10685  infssfzledc  10686  nfseq  10914  seq3f1olemstep  10971  seq3f1olemp  10972  nfwrd  11354  reuccatpfxs1v  11541  fimaxre2  12015  nfsum1  12146  nfsum  12147  cbvsumv  12151  cbvsumi  12152  sumfct  12164  sumrbdclem  12168  summodclem2a  12172  zsumdc  12175  fsum3  12178  isumss  12182  isumss2  12184  fsum3cvg2  12185  fsumzcl2  12196  fsumadd  12197  fsumsplitf  12199  sumsnf  12200  sumsn  12202  sumsns  12206  fsumsplitsnun  12210  fsum2dlemstep  12225  fisumcom2  12229  fsumshftm  12236  fsum00  12253  fsumrelem  12262  fsumiun  12268  mertenslem2  12327  prodeq1  12344  nfcprod1  12345  nfcprod  12346  cbvprod  12349  cbvprodv  12350  cbvprodi  12351  prodrbdclem  12362  prodmodclem2a  12367  zproddc  12370  fprodseq  12374  fprodntrivap  12375  prodfct  12378  prodssdc  12380  prodsnf  12383  prodsn  12384  fprodm1s  12392  fprodp1s  12393  prodsns  12394  fprodcllemf  12404  fprodconst  12411  fprodap0  12412  fprod2dlemstep  12413  fprodcom2fi  12417  fprodrec  12420  fproddivapf  12422  fprodsplitf  12423  fprodap0f  12427  fprodle  12431  bezoutlemmain  12799  bezout  12812  nnwofdc  12839  nnwosdc  12840  prmind2  12922  nnmaxpwlemdvds  12973  nnmaxpwlemndvds  12974  pcmpt  13150  pcmptdvds  13152  ctiunctlemudc  13385  ctiunctlemf  13386  ctiunctlemfo  13387  ctiunct  13388  ctiunctal  13389  gzsumconstf  14233  gzsumsplit0  14237  gsumsncmn  14245  gsummptfidmadd  14250  gsumsnfdcmn  14256  gsumsndcmn  14257  gsumunsnd  14259  gsum2d2fi  14273  gsumcom2fi  14274  prdsbas3  14293  psrass1filem  15186  cnmpt11  15526  cnmpt1t  15528  cnmpt21  15534  cnmpt2t  15536  cnmptcom  15541  imasnopn  15542  fsumcncntop  15810  ellimc3apf  15903  ellimc3ap  15904  limcmpted  15906  dvmptfsum  15968  elplyd  15984  fsumdvdsmul  16302  lgseisenlem2  16412  gropd  16510  grstructd2dom  16511  lfgrnloopen  16596  elabf1  17031  elabf2  17032  elabg2  17035  bj-omssind  17183  bj-bdfindisg  17196  bj-nntrans  17199  bj-nnelirr  17201  bj-omtrans  17204  setindis  17215  bdsetindis  17217  bj-nn0sucALT  17226  bj-findis  17227  bj-findisg  17228  strcollnfALT  17234  isomninnlem  17302  trilpolemeq1  17313  trirec0  17317  iswomninnlem  17323  ismkvnnlem  17326  nconstwlpolemgt0  17338