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  7332  nfdju  7382  exmidomni  7482  ismkvnex  7495  cc2  7633  cc4f  7635  cc4  7636  caucvgprprlemaddq  8075  caucvgsrlemgt1  8162  axpre-suploclemres  8268  lble  9279  supinfneg  10004  infsupneg  10005  fzrevral  10522  zsupcllemstep  10672  infssuzex  10676  infssuzcldc  10678  infssfzcldc  10679  infssfzledc  10680  nfseq  10907  seq3f1olemstep  10964  seq3f1olemp  10965  nfwrd  11347  reuccatpfxs1v  11534  fimaxre2  12008  nfsum1  12138  nfsum  12139  cbvsumv  12143  cbvsumi  12144  sumfct  12156  sumrbdclem  12160  summodclem2a  12164  zsumdc  12167  fsum3  12170  isumss  12174  isumss2  12176  fsum3cvg2  12177  fsumzcl2  12188  fsumadd  12189  fsumsplitf  12191  sumsnf  12192  sumsn  12194  sumsns  12198  fsumsplitsnun  12202  fsum2dlemstep  12217  fisumcom2  12221  fsumshftm  12228  fsum00  12245  fsumrelem  12254  fsumiun  12260  mertenslem2  12319  prodeq1  12336  nfcprod1  12337  nfcprod  12338  cbvprod  12341  cbvprodv  12342  cbvprodi  12343  prodrbdclem  12354  prodmodclem2a  12359  zproddc  12362  fprodseq  12366  fprodntrivap  12367  prodfct  12370  prodssdc  12372  prodsnf  12375  prodsn  12376  fprodm1s  12384  fprodp1s  12385  prodsns  12386  fprodcllemf  12396  fprodconst  12403  fprodap0  12404  fprod2dlemstep  12405  fprodcom2fi  12409  fprodrec  12412  fproddivapf  12414  fprodsplitf  12415  fprodap0f  12419  fprodle  12423  bezoutlemmain  12791  bezout  12804  nnwofdc  12831  nnwosdc  12832  prmind2  12914  nnmaxpwlemdvds  12965  nnmaxpwlemndvds  12966  pcmpt  13142  pcmptdvds  13144  ctiunctlemudc  13377  ctiunctlemf  13378  ctiunctlemfo  13379  ctiunct  13380  ctiunctal  13381  gzsumconstf  14193  gzsumsplit0  14197  gsumsncmn  14205  gsummptfidmadd  14210  prdsbas3  14236  cnmpt11  15433  cnmpt1t  15435  cnmpt21  15441  cnmpt2t  15443  cnmptcom  15448  imasnopn  15449  fsumcncntop  15717  ellimc3apf  15810  ellimc3ap  15811  limcmpted  15813  dvmptfsum  15875  elplyd  15891  fsumdvdsmul  16186  lgseisenlem2  16288  gropd  16386  grstructd2dom  16387  lfgrnloopen  16472  elabf1  16907  elabf2  16908  elabg2  16911  bj-omssind  17059  bj-bdfindisg  17072  bj-nntrans  17075  bj-nnelirr  17077  bj-omtrans  17080  setindis  17091  bdsetindis  17093  bj-nn0sucALT  17102  bj-findis  17103  bj-findisg  17104  strcollnfALT  17110  isomninnlem  17177  trilpolemeq1  17187  trirec0  17191  iswomninnlem  17197  ismkvnnlem  17200  nconstwlpolemgt0  17212