Theorem nfsbc1v 3762

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

This proof depends on syntax axioms:  Ⅎwnf 1815  [wsbc 3742

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-sbc 3743

This theorem is used by:  elrabsf  3787  cbvralcsf  3893  reusngf  4635  rexreusng  4640  reuprg0  4663  rmosn  4680  rabsnifsb  4683  euotd  5490  reuop  6303  frpoinsg  6353  elfvmptrab1w  7032  elfvmptrab1  7033  ralrnmptw  7105  ralrnmpt  7107  oprabv  7490  elovmporab  7677  elovmporab1w  7678  elovmporab1  7679  ovmpt3rabdm  7690  elovmpt3rab1  7691  tfisg  7875  tfindes  7884  findes  7922  dfopab2  8074  dfoprab3s  8075  ralxpes  8166  ralxp3es  8169  frpoins3xpg  8170  frpoins3xp3g  8171  mpoxopoveq  8250  findcard2  9194  ac6sfi  9289  indexfi  9363  setinds  9763  frinsg  9768  nn0ind-raph  12812  uzind4s  13048  fzrevral  13759  rabssnn0fi  14142  prmind2  16875  elmptrab  24161  isfildlem  24191  2sqreulem4  27796  gropd  29624  grstructd  29625  rspc2daf  33120  opreu2reuALT  33130  bnj919  35454  bnj1468  35532  bnj110  35544  bnj607  35602  bnj873  35610  bnj849  35611  bnj1388  35719  bnj1489  35742  rdgssun  38444  indexa  38810  indexdom  38811  sdclem2  38819  sdclem1  38820  fdc1  38823  alrimii  39194  riotasv2s  40158  sbccomieg  43943  rexrabdioph  43944  rexfrabdioph  43945  aomclem6  44204  pm14.24  45558  or2expropbilem2  48245  or2expropbi  48246  ich2exprop  48695  ichnreuop  48696  ichreuopeq  48697  prproropreud  48733  reupr  48746  reuopreuprim  48750