ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfcv Unicode version

Theorem nfcv 2223
Description: If  x is disjoint from  A, then  x is not free in  A. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfcv  |-  F/_ x A
Distinct variable group:    x, A

Proof of Theorem nfcv
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 nfv 1462 . 2  |-  F/ x  y  e.  A
21nfci 2213 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    e. wcel 1434   F/_wnfc 2210
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1379  ax-17 1460
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-nfc 2212
This theorem is referenced by:  nfcvd  2224  nfel  2231  nfeq1  2232  nfel1  2233  nfeq2  2234  nfel2  2235  nfcvf  2244  r2al  2391  r2ex  2392  nfraldxy  2404  nfrexdxy  2405  nfra2xy  2412  r19.12  2472  ralcom  2523  rexcom  2524  nfreudxy  2533  raleq  2555  rexeq  2556  reueq1  2557  rmoeq1  2558  cbvral  2579  cbvrex  2580  rabeq  2603  rabeqi  2604  cbvrabv  2610  vtoclg  2668  vtocl2g  2672  vtoclga  2674  vtocl2ga  2676  vtocl3ga  2678  spcimdv  2692  spcimedv  2694  spcgv  2695  spcegv  2696  rspct  2704  rspc  2705  rspce  2706  rspc2  2720  ceqsexg  2732  elabgt  2744  elabf  2746  elabg  2748  elab3g  2753  elrab  2758  mob  2784  nfsbc1v  2843  elrabsf  2862  sbcralt  2900  sbcrext  2901  sbcralg  2902  sbcrex  2903  sbcreug  2904  cbvcsbv  2923  csbconstg  2930  nfcsb1v  2948  csbnestg  2966  cbvralcsf  2974  cbvrexcsf  2975  cbvreucsf  2976  cbvrabcsf  2977  cbvralv2  2978  cbvrexv2  2979  n0rf  3277  n0r  3278  eq0  3283  raaanlem  3364  nfpw  3413  cbviunv  3738  cbviinv  3739  ssiun2s  3743  iunab  3745  ssiinf  3748  ssiin  3749  iinab  3760  cbvdisjv  3798  nfdisjv  3799  cbvmptv  3894  triun  3909  csbexga  3927  repizf2  3957  moop2  4035  euotd  4038  opelopabf  4058  nfpo  4085  nfso  4086  pofun  4096  nfse  4125  nffrfor  4132  nffr  4133  frind  4136  nfwe  4139  eusvnf  4232  rabxfrd  4248  tfis  4353  tfisi  4357  opeliunxp  4442  nfrel  4472  opeliunxp2  4525  ralxpf  4531  rexxpf  4532  nfco  4550  nfcnv  4563  dfdmf  4577  dfrnf  4624  nfdm  4627  nfres  4663  nfiotadxy  4921  dffun6f  4966  dffun6  4967  dffun4f  4969  nffun  4975  funimaexglem  5034  nffv  5238  nffvmpt1  5239  dffn5imf  5282  funfvdm2f  5292  fvmptss2  5301  fvmpts  5304  fvmpt2  5308  fvmptssdm  5309  mptfvex  5310  fvmptdv  5313  eqfnfv2f  5323  ralrnmpt  5363  rexrnmpt  5364  f1ompt  5374  ffnfvf  5378  fmptco  5384  fmptcof  5385  fmptcos  5386  funiunfvdmf  5457  dff13f  5463  f1mpt  5464  fliftfuns  5491  nfiso  5499  nfriotadxy  5529  csbriotag  5533  riota2  5543  mpt2eq123  5617  cbvmpt2x  5635  cbvmpt2  5636  cbvmpt2v  5637  ovmpt2s  5677  ov2gf  5678  ovmpt2dxf  5679  ovmpt2dx  5680  ovmpt2dv  5686  ovmpt2dv2  5687  ovi3  5690  nfof  5770  nfofr  5771  offval2  5779  ofrfval2  5780  abrexex2g  5800  abrexex2  5804  dfopab2  5868  dfoprab3s  5869  mpt2mptsx  5876  dmmpt2ssx  5878  fmpt2x  5879  mpt2fvex  5882  fmpt2co  5890  dfmpt2  5897  f1od2  5909  mpt2xopoveq  5911  mpt2xopovel  5912  nftpos  5950  tposoprab  5951  nfrecs  5978  nffrec  6067  eqerlem  6226  qliftfuns  6279  dom2lem  6342  xpcomco  6393  xpf1o  6408  ac6sfi  6456  nfsup  6501  nfdju  6553  exmidomni  6583  caucvgprprlemaddq  7037  caucvgsrlemgt1  7110  lble  8169  supinfneg  8841  infsupneg  8842  fzrevral  9275  nfiseq  9605  fimaxre2  10335  nfsum1  10419  nfsum  10420  zsupcllemstep  10573  infssuzex  10577  infssuzcldc  10579  bezoutlemmain  10619  bezout  10632  prmind2  10734  oddpwdclemdvds  10780  oddpwdclemndvds  10781  elabf1  10876  elabf2  10877  elabg2  10880  bj-omssind  11022  bj-bdfindisg  11035  bj-nntrans  11038  bj-nnelirr  11040  bj-omtrans  11043  setindis  11054  bdsetindis  11056  bj-nn0sucALT  11065  bj-findis  11066  bj-findisg  11067  strcollnfALT  11073
  Copyright terms: Public domain W3C validator