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

Theorem nfsbc1v 2979
Description: Bound-variable hypothesis builder for class substitution. (Contributed by Mario Carneiro, 12-Oct-2016.)
Assertion
Ref Expression
nfsbc1v 𝑥[𝐴 / 𝑥]𝜑
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem nfsbc1v
StepHypRef Expression
1 nfcv 2317 . 2 𝑥𝐴
21nfsbc1 2978 1 𝑥[𝐴 / 𝑥]𝜑
Colors of variables: wff set class
Syntax hints:  wnf 1458  [wsbc 2960
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-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-sbc 2961
This theorem is referenced by:  elrabsf  2999  cbvralcsf  3117  cbvrexcsf  3118  euotd  4248  findes  4596  omsinds  4615  elfvmptrab1  5602  ralrnmpt  5650  rexrnmpt  5651  dfopab2  6180  dfoprab3s  6181  mpoxopoveq  6231  findcard2  6879  findcard2s  6880  ac6sfi  6888  dcfi  6970  indpi  7316  nn0ind-raph  9341  uzind4s  9561  indstr  9564  fzrevral  10073  exfzdc  10208  uzsinds  10410  zsupcllemstep  11912  infssuzex  11916  prmind2  12086  bj-bdfindes  14183  bj-findes  14215
  Copyright terms: Public domain W3C validator