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

Theorem nfsbcw 3810
Description: Bound-variable hypothesis builder for class substitution. Version of nfsbc 3813 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by NM, 7-Sep-2014.) Avoid ax-13 2377. (Revised by GG, 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 1804 . . 3 𝑦
2 nfsbcw.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfsbcw.2 . . . 4 𝑥𝜑
54a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
61, 3, 5nfsbcdw 3809 . 2 (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝜑)
76mptru 1547 1 𝑥[𝐴 / 𝑦]𝜑
Colors of variables: wff setvar class
Syntax hints:  wtru 1541  wnf 1783  wnfc 2890  [wsbc 3788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-sbc 3789
This theorem is referenced by:  opelopabgf  5545  opelopabf  5550  ralrnmptw  7114  elovmporab  7679  elovmporab1w  7680  ovmpt3rabdm  7692  elovmpt3rab1  7693  dfopab2  8077  dfoprab3s  8078  ralxpes  8161  ralxp3es  8164  frpoins3xpg  8165  frpoins3xp3g  8166  mpoxopoveq  8244  elmptrab  23835  bnj1445  35058  bnj1446  35059  bnj1467  35068  indexa  37740  sdclem1  37750  sbcalf  38121  sbcexf  38122  sbccomieg  42804  rexrabdioph  42805  or2expropbilem2  47045  or2expropbi  47046  ich2exprop  47458  ichnreuop  47459  reuopreuprim  47513
  Copyright terms: Public domain W3C validator