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

Theorem nfcvd 2179
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 2178 . 2 𝑥𝐴
21a1i 9 1 (𝜑𝑥𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wnfc 2165
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338  ax-17 1419
This theorem depends on definitions:  df-bi 110  df-nf 1350  df-nfc 2167
This theorem is referenced by:  nfeld  2193  vtoclgft  2604  vtocld  2606  sbcralt  2834  sbcrext  2835  csbied  2892  csbie2t  2894  sbcco3g  2903  csbco3g  2904  dfnfc2  3598  eusvnfb  4186  eusv2i  4187  peano2  4318  iota2d  4892  iota2  4893  fmptcof  5331  riota5f  5492  riota5  5493  fmpt2co  5837  nfnegd  7205  strcollnft  10083
  Copyright terms: Public domain W3C validator