Theorem nfsbc1v 3759

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

This proof depends on syntax axioms:  Ⅎwnf 1816  [wsbc 3739

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-sbc 3740

This theorem is used by:  elrabsf  3784  cbvralcsf  3889  reusngf  4635  rexreusng  4640  reuprg0  4663  rmosn  4680  rabsnifsb  4683  euotd  5486  reuop  6296  frpoinsg  6346  elfvmptrab1w  7021  elfvmptrab1  7022  ralrnmptw  7094  ralrnmpt  7096  oprabv  7480  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  ovmpt3rabdm  7680  elovmpt3rab1  7681  tfisg  7865  tfindes  7874  findes  7912  dfopab2  8063  dfoprab3s  8064  ralxpes  8153  ralxp3es  8156  frpoins3xpg  8157  frpoins3xp3g  8158  mpoxopoveq  8236  findcard2  9180  ac6sfi  9275  indexfi  9349  setinds  9750  frinsg  9755  nn0ind-raph  12799  uzind4s  13035  fzrevral  13746  rabssnn0fi  14129  prmind2  16860  elmptrab  24146  isfildlem  24176  2sqreulem4  27781  gropd  29609  grstructd  29610  rspc2daf  33063  opreu2reuALT  33073  bnj919  35398  bnj1468  35476  bnj110  35488  bnj607  35546  bnj873  35554  bnj849  35555  bnj1388  35663  bnj1489  35686  dfon2lem1  36545  rdgssun  38301  indexa  38667  indexdom  38668  sdclem2  38676  sdclem1  38677  fdc1  38680  alrimii  39051  riotasv2s  40015  sbccomieg  43799  rexrabdioph  43800  rexfrabdioph  43801  aomclem6  44060  pm14.24  45415  or2expropbilem2  48102  or2expropbi  48103  ich2exprop  48552  ichnreuop  48553  ichreuopeq  48554  prproropreud  48590  reupr  48603  reuopreuprim  48607