Theorem nfsbc1v 3050

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

Step	Hyp	Ref	Expression
1		nfcv 2374	. 2 ⊢ Ⅎ𝑥𝐴
2	1	nfsbc1 3049	1 ⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1508  [wsbc 3031

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-sbc 3032

This theorem is referenced by:  elrabsf  3070  cbvralcsf  3190  cbvrexcsf  3191  rabsnifsb  3737  euotd  4347  findes  4701  omsinds  4720  elfvmptrab1  5741  ralrnmpt  5789  rexrnmpt  5790  elovmporab  6222  elovmporab1w  6223  uchoice  6300  dfopab2  6352  dfoprab3s  6353  mpoxopoveq  6406  findcard2  7078  findcard2s  7079  ac6sfi  7087  opabfi  7132  dcfi  7180  indpi  7562  nn0ind-raph  9597  uzind4s  9824  indstr  9827  fzrevral  10340  exfzdc  10487  zsupcllemstep  10490  infssuzex  10494  uzsinds  10707  prmind2  12697  gropd  15904  grstructd2dom  15905  bj-bdfindes  16570  bj-findes  16602