![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfsbcw | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for class substitution. Version of nfsbc 3803 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 7-Sep-2014.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.) |
Ref | Expression |
---|---|
nfsbcw.1 | ⊢ Ⅎ𝑥𝐴 |
nfsbcw.2 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfsbcw | ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nftru 1807 | . . 3 ⊢ Ⅎ𝑦⊤ | |
2 | nfsbcw.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐴) |
4 | nfsbcw.2 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
5 | 4 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜑) |
6 | 1, 3, 5 | nfsbcdw 3799 | . 2 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝜑) |
7 | 6 | mptru 1549 | 1 ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1543 Ⅎwnf 1786 Ⅎwnfc 2884 [wsbc 3778 |
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 |
This theorem is referenced by: opelopabgf 5541 opelopabf 5546 ralrnmptw 7096 elovmporab 7652 elovmporab1w 7653 ovmpt3rabdm 7665 elovmpt3rab1 7666 dfopab2 8038 dfoprab3s 8039 ralxpes 8122 ralxp3es 8125 frpoins3xpg 8126 frpoins3xp3g 8127 mpoxopoveq 8204 elmptrab 23331 bnj1445 34086 bnj1446 34087 bnj1467 34096 indexa 36649 sdclem1 36659 sbcalf 37030 sbcexf 37031 sbccomieg 41579 rexrabdioph 41580 or2expropbilem2 45791 or2expropbi 45792 ich2exprop 46187 ichnreuop 46188 reuopreuprim 46242 |
Copyright terms: Public domain | W3C validator |