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

Theorem nfcvd 2241
Description: If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 7-Oct-2016.)
Assertion
Ref Expression
nfcvd (𝜑𝑥𝐴)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem nfcvd
StepHypRef Expression
1 nfcv 2240 . 2 𝑥𝐴
21a1i 9 1 (𝜑𝑥𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wnfc 2227
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1393  ax-17 1474
This theorem depends on definitions:  df-bi 116  df-nf 1405  df-nfc 2229
This theorem is referenced by:  nfeld  2256  vtoclgft  2691  vtocld  2693  sbcralt  2937  sbcrext  2938  csbied  2996  csbie2t  2998  sbcco3g  3007  csbco3g  3008  dfnfc2  3701  eusvnfb  4313  eusv2i  4314  peano2  4447  iota2d  5049  iota2  5050  fmptcof  5519  riota5f  5686  riota5  5687  fmpoco  6043  nfixpxy  6541  nfnegd  7829  iseqf1olemjpcl  10109  iseqf1olemqpcl  10110  iseqf1olemfvp  10111  seq3f1olemqsum  10114  strcollnft  12767
  Copyright terms: Public domain W3C validator