MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfcsbw Structured version   Visualization version   GIF version

Theorem nfcsbw 3883
Description: Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3884 with a disjoint variable condition, which does not require ax-13 2391. (Contributed by Mario Carneiro, 12-Oct-2016.) (Revised by Gino Giotto, 10-Jan-2024.)
Hypotheses
Ref Expression
nfcsbw.1 𝑥𝐴
nfcsbw.2 𝑥𝐵
Assertion
Ref Expression
nfcsbw 𝑥𝐴 / 𝑦𝐵
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem nfcsbw
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-csb 3858 . . 3 𝐴 / 𝑦𝐵 = {𝑧[𝐴 / 𝑦]𝑧𝐵}
2 nftru 1806 . . . 4 𝑧
3 nftru 1806 . . . . 5 𝑦
4 nfcsbw.1 . . . . . 6 𝑥𝐴
54a1i 11 . . . . 5 (⊤ → 𝑥𝐴)
6 nfcsbw.2 . . . . . . 7 𝑥𝐵
76a1i 11 . . . . . 6 (⊤ → 𝑥𝐵)
87nfcrd 2966 . . . . 5 (⊤ → Ⅎ𝑥 𝑧𝐵)
93, 5, 8nfsbcdw 3770 . . . 4 (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝑧𝐵)
102, 9nfabdw 2995 . . 3 (⊤ → 𝑥{𝑧[𝐴 / 𝑦]𝑧𝐵})
111, 10nfcxfrd 2973 . 2 (⊤ → 𝑥𝐴 / 𝑦𝐵)
1211mptru 1545 1 𝑥𝐴 / 𝑦𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1539  wcel 2115  {cab 2799  wnfc 2958  [wsbc 3749  csb 3857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-sbc 3750  df-csb 3858
This theorem is referenced by:  cbvrabcsfw  3898  elfvmptrab1w  6767  fmptcof  6865  fvmpopr2d  7285  elovmporab1w  7367  mpomptsx  7737  dmmpossx  7739  fmpox  7740  el2mpocsbcl  7755  fmpoco  7765  dfmpo  7772  mpocurryd  7910  fvmpocurryd  7912  nfsum  15026  fsum2dlem  15104  fsumcom2  15108  nfcprod  15244  fprod2dlem  15313  fprodcom2  15317  fsumcn  23454  fsum2cn  23455  dvmptfsum  24557  itgsubst  24631  iundisj2f  30327  f1od2  30444  esumiun  31361  poimirlem26  34965  cdlemkid  38114  cdlemk19x  38121  cdlemk11t  38124  wdom2d2  39783  dmmpossx2  44557
  Copyright terms: Public domain W3C validator