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

Theorem nfcsbw 3921
Description: Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3922 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Mario Carneiro, 12-Oct-2016.) Avoid ax-13 2372. (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 3895 . . 3 𝐴 / 𝑦𝐵 = {𝑧[𝐴 / 𝑦]𝑧𝐵}
2 nftru 1807 . . . 4 𝑧
3 nftru 1807 . . . . 5 𝑦
4 nfcsbw.1 . . . . . 6 𝑥𝐴
54a1i 11 . . . . 5 (⊤ → 𝑥𝐴)
6 nfcsbw.2 . . . . . . 7 𝑥𝐵
76a1i 11 . . . . . 6 (⊤ → 𝑥𝐵)
87nfcrd 2893 . . . . 5 (⊤ → Ⅎ𝑥 𝑧𝐵)
93, 5, 8nfsbcdw 3799 . . . 4 (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝑧𝐵)
102, 9nfabdw 2927 . . 3 (⊤ → 𝑥{𝑧[𝐴 / 𝑦]𝑧𝐵})
111, 10nfcxfrd 2903 . 2 (⊤ → 𝑥𝐴 / 𝑦𝐵)
1211mptru 1549 1 𝑥𝐴 / 𝑦𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1543  wcel 2107  {cab 2710  wnfc 2884  [wsbc 3778  csb 3894
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-sbc 3779  df-csb 3895
This theorem is referenced by:  cbvrabcsfw  3938  elfvmptrab1w  7025  fmptcof  7128  fvmpopr2d  7569  elovmporab1w  7653  mpomptsx  8050  dmmpossx  8052  fmpox  8053  el2mpocsbcl  8071  fmpoco  8081  dfmpo  8088  mpocurryd  8254  fvmpocurryd  8256  nfsum  15637  fsum2dlem  15716  fsumcom2  15720  nfcprod  15855  fprod2dlem  15924  fprodcom2  15928  fsumcn  24386  fsum2cn  24387  dvmptfsum  25492  itgsubst  25566  iundisj2f  31821  f1od2  31946  esumiun  33092  poimirlem26  36514  cdlemkid  39807  cdlemk19x  39814  cdlemk11t  39817  fmpocos  41056  wdom2d2  41774  dmmpossx2  47012
  Copyright terms: Public domain W3C validator