Theorem nfsbc1v 3743

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 2901	. 2 ⊢ Ⅎ𝑥𝐴
2	1	nfsbc1 3742	1 ⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1790  [wsbc 3723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-sbc 3724

This theorem is referenced by:  elrabsf  3768  cbvralcsf  3873  reusngf  4607  rexreusng  4612  reuprg0  4635  rmosn  4652  rabsnifsb  4655  euotd  5455  reuop  6245  frpoinsg  6295  elfvmptrab1w  6964  elfvmptrab1  6965  ralrnmptw  7036  ralrnmpt  7038  oprabv  7417  elovmporab  7603  elovmporab1w  7604  elovmporab1  7605  ovmpt3rabdm  7616  elovmpt3rab1  7617  tfisg  7795  tfindes  7804  findes  7841  dfopab2  7995  dfoprab3s  7996  ralxpes  8077  ralxp3es  8080  frpoins3xpg  8081  frpoins3xp3g  8082  mpoxopoveq  8160  findcard2  9090  ac6sfi  9185  indexfi  9261  setinds  9662  frinsg  9667  nn0ind-raph  12621  uzind4s  12850  fzrevral  13558  rabssnn0fi  13940  prmind2  16646  elmptrab  23811  isfildlem  23841  2sqreulem4  27436  gropd  29119  grstructd  29120  rspc2daf  32554  opreu2reuALT  32565  bnj919  34959  bnj1468  35037  bnj110  35049  bnj607  35107  bnj873  35115  bnj849  35116  bnj1388  35224  bnj1489  35247  dfon2lem1  36018  rdgssun  37749  indexa  38109  indexdom  38110  sdclem2  38118  sdclem1  38119  fdc1  38122  alrimii  38495  riotasv2s  39459  sbccomieg  43247  rexrabdioph  43248  rexfrabdioph  43249  aomclem6  43513  pm14.24  44885  or2expropbilem2  47504  or2expropbi  47505  ich2exprop  47954  ichnreuop  47955  ichreuopeq  47956  prproropreud  47992  reupr  48005  reuopreuprim  48009