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

Theorem nfsbcw 3774
 Description: Bound-variable hypothesis builder for class substitution. Version of nfsbc 3777 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 7-Sep-2014.) (Revised by Gino Giotto, 10-Jan-2024.)
Hypotheses
Ref Expression
nfsbcw.1 𝑥𝐴
nfsbcw.2 𝑥𝜑
Assertion
Ref Expression
nfsbcw 𝑥[𝐴 / 𝑦]𝜑
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)

Proof of Theorem nfsbcw
StepHypRef Expression
1 nftru 1805 . . 3 𝑦
2 nfsbcw.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfsbcw.2 . . . 4 𝑥𝜑
54a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
61, 3, 5nfsbcdw 3773 . 2 (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝜑)
76mptru 1544 1 𝑥[𝐴 / 𝑦]𝜑
 Colors of variables: wff setvar class Syntax hints:  ⊤wtru 1538  Ⅎwnf 1784  Ⅎwnfc 2957  [wsbc 3752 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-sbc 3753 This theorem is referenced by:  opelopabgf  5403  opelopabf  5408  ralrnmptw  6836  elovmporab  7369  elovmporab1w  7370  ovmpt3rabdm  7382  elovmpt3rab1  7383  dfopab2  7728  dfoprab3s  7729  mpoxopoveq  7863  elmptrab  22411  bnj1445  32324  bnj1446  32325  bnj1467  32334  indexa  35047  sdclem1  35057  sbcalf  35428  sbcexf  35429  sbccomieg  39527  rexrabdioph  39528  or2expropbilem2  43416  or2expropbi  43417  ich2exprop  43779  ichnreuop  43780  reuopreuprim  43834
 Copyright terms: Public domain W3C validator