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  2741  rexeq  2742  reueq1  2743  rmoeq1  2744  cbvralw  2771  cbvrexw  2772  cbvral  2774  cbvrex  2775  rabeq  2805  rabeqi  2806  cbvrabv  2812  vtoclg  2875  vtocl2g  2879  vtoclga  2881  vtocl2ga  2883  vtocl3ga  2885  spcimdv  2901  spcimedv  2903  spcgv  2904  spcegv  2905  rspct  2914  rspc  2915  rspce  2916  rspc2  2932  ceqsexg  2945  elabgt  2958  elabf  2960  elabg  2963  elab3g  2968  elrab  2973  mob  2999  nfsbc1v  3061  elrabsf  3081  sbcralt  3119  sbcrext  3120  sbcralg  3121  sbcrex  3122  sbcreug  3123  reu8nf  3124  cbvcsbv  3144  csbconstg  3152  nfcsb1v  3171  csbie  3184  csbnestg  3193  cbvralcsf  3201  cbvrexcsf  3202  cbvreucsf  3203  cbvrabcsf  3204  cbvralv2  3205  cbvrexv2  3206  dfss4st  3454  n0rf  3521  n0r  3522  eq0  3527  raaanlem  3614  nfpw  3685  cbviunv  4030  cbviinv  4031  ssiun2s  4035  iunab  4038  ssiinf  4041  ssiin  4042  iinab  4053  cbvdisjv  4096  nfdisjv  4097  disjnims  4100  disji2  4101  invdisjrab  4103  cbvmptv  4206  triun  4221  csbexga  4238  repizf2  4275  moop2  4368  euotd  4371  opelopabgf  4388  opelopabf  4393  nfpo  4422  nfso  4423  pofun  4433  nfse  4462  nffrfor  4469  nffr  4470  frind  4473  nfwe  4476  eusvnf  4574  rabxfrd  4590  tfis  4705  tfisi  4709  opeliunxp  4805  nfrel  4835  opeliunxp2  4895  ralxpf  4901  rexxpf  4902  nfco  4920  nfcnv  4934  dfdmf  4949  dfrnf  4998  nfdm  5001  nfres  5040  resmptf  5088  nfiotadw  5315  dffun6f  5365  dffun6  5366  dffun4f  5368  nffun  5375  funimaexglem  5439  nffv  5680  nffvmpt1  5681  dffn5imf  5732  funfvdm2f  5742  fvmptss2  5752  fvmpts  5755  fvmpt2  5761  fvmptssdm  5762  mptfvex  5763  fvmptdv  5766  fvmptd3  5771  elfvmptrab1  5772  eqfnfv2f  5779  ralrnmpt  5819  rexrnmpt  5820  f1ompt  5828  ffnfvf  5836  fmptco  5843  fmptcof  5844  fmptcos  5845  funiunfvdmf  5937  dff13f  5943  f1mpt  5944  fliftfuns  5971  nfiso  5979  nfriotadxy  6012  csbriotag  6017  riota2  6027  mpoeq123  6112  cbvmpox  6131  cbvmpo  6132  cbvmpov  6133  ovmpos  6177  ov2gf  6178  ovmpodxf  6179  ovmpodx  6180  ovmpodv  6186  ovmpodv2  6187  fvmpopr2d  6190  ovi3  6191  elovmporab  6254  elovmporab1w  6255  nfof  6272  nfofr  6273  offval2  6282  ofrfval2  6283  abrexex2g  6313  abrexex2  6317  uchoice  6331  dfopab2  6383  dfoprab3s  6384  mpomptsx  6393  dmmpossx  6395  fmpox  6396  mpofvex  6401  fnmpoovd  6411  fmpoco  6412  dfmpo  6419  f1od2  6431  disjxp1  6432  mpoxopoveq  6471  mpoxopovel  6472  nftpos  6510  tposoprab  6511  nfrecs  6538  nffrec  6627  eqerlem  6798  qliftfuns  6853  cbvixpv  6951  nfixpxy  6952  nfixp1  6953  ixpf  6955  mptelixpg  6969  dom2lem  7011  modom  7061  xpcomco  7077  xpf1o  7097  mapxpen  7101  ac6sfi  7155  opabfi  7200  nfsup  7283  nfdju  7333  exmidomni  7433  ismkvnex  7446  cc2  7581  cc4f  7583  cc4  7584  caucvgprprlemaddq  8023  caucvgsrlemgt1  8110  axpre-suploclemres  8216  lble  9221  supinfneg  9927  infsupneg  9928  fzrevral  10439  zsupcllemstep  10589  infssuzex  10593  infssuzcldc  10595  nfseq  10819  seq3f1olemstep  10876  seq3f1olemp  10877  nfwrd  11253  reuccatpfxs1v  11440  fimaxre2  11912  nfsum1  12041  nfsum  12042  cbvsumv  12046  cbvsumi  12047  sumfct  12059  sumrbdclem  12063  summodclem2a  12067  zsumdc  12070  fsum3  12073  isumss  12077  isumss2  12079  fsum3cvg2  12080  fsumzcl2  12091  fsumadd  12092  fsumsplitf  12094  sumsnf  12095  sumsn  12097  sumsns  12101  fsumsplitsnun  12105  fsum2dlemstep  12120  fisumcom2  12124  fsumshftm  12131  fsum00  12148  fsumrelem  12157  fsumiun  12163  mertenslem2  12222  prodeq1  12239  nfcprod1  12240  nfcprod  12241  cbvprod  12244  cbvprodv  12245  cbvprodi  12246  prodrbdclem  12257  prodmodclem2a  12262  zproddc  12265  fprodseq  12269  fprodntrivap  12270  prodfct  12273  prodssdc  12275  prodsnf  12278  prodsn  12279  fprodm1s  12287  fprodp1s  12288  prodsns  12289  fprodcllemf  12299  fprodconst  12306  fprodap0  12307  fprod2dlemstep  12308  fprodcom2fi  12312  fprodrec  12315  fproddivapf  12317  fprodsplitf  12318  fprodap0f  12322  fprodle  12326  bezoutlemmain  12694  bezout  12707  nnwofdc  12734  nnwosdc  12735  prmind2  12817  oddpwdclemdvds  12867  oddpwdclemndvds  12868  pcmpt  13041  pcmptdvds  13043  ctiunctlemudc  13188  ctiunctlemf  13189  ctiunctlemfo  13190  ctiunct  13191  ctiunctal  13192  prdsbas3  13500  gsumfzconstf  14059  gsumsplit0  14063  cnmpt11  15148  cnmpt1t  15150  cnmpt21  15156  cnmpt2t  15158  cnmptcom  15163  imasnopn  15164  fsumcncntop  15432  ellimc3apf  15525  ellimc3ap  15526  limcmpted  15528  dvmptfsum  15590  elplyd  15606  fsumdvdsmul  15859  lgseisenlem2  15944  gropd  16042  grstructd2dom  16043  lfgrnloopen  16128  elabf1  16553  elabf2  16554  elabg2  16557  bj-omssind  16705  bj-bdfindisg  16718  bj-nntrans  16721  bj-nnelirr  16723  bj-omtrans  16726  setindis  16737  bdsetindis  16739  bj-nn0sucALT  16748  bj-findis  16749  bj-findisg  16750  strcollnfALT  16756  isomninnlem  16814  trilpolemeq1  16824  trirec0  16828  iswomninnlem  16834  ismkvnnlem  16837  nconstwlpolemgt0  16850  gfsumsn  16867