Theorem nfsbc1v 2973

Description: Bound-variable hypothesis builder for class substitution. (Contributed by Mario Carneiro, 12-Oct-2016.)

Assertion

Ref	Expression
nfsbc1v	|- F/ x [. A / x ]. ph

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem nfsbc1v

Step	Hyp	Ref	Expression
1		nfcv 2312	. 2 |- F/_ x A
2	1	nfsbc1 2972	1 |- F/ x [. A / x ]. ph

Syntax hints:   F/wnf 1453   [.wsbc 2955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-sbc 2956

This theorem is referenced by:  elrabsf  2993  cbvralcsf  3111  cbvrexcsf  3112  euotd  4239  findes  4587  omsinds  4606  elfvmptrab1  5590  ralrnmpt  5638  rexrnmpt  5639  dfopab2  6168  dfoprab3s  6169  mpoxopoveq  6219  findcard2  6867  findcard2s  6868  ac6sfi  6876  dcfi  6958  indpi  7304  nn0ind-raph  9329  uzind4s  9549  indstr  9552  fzrevral  10061  exfzdc  10196  uzsinds  10398  zsupcllemstep  11900  infssuzex  11904  prmind2  12074  bj-bdfindes  13984  bj-findes  14016