![]() |
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 3802 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by NM, 7-Sep-2014.) Avoid ax-13 2370. (Revised by Gino Giotto, 10-Jan-2024.) |
Ref | Expression |
---|---|
nfsbcw.1 | ⊢ Ⅎ𝑥𝐴 |
nfsbcw.2 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfsbcw | ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nftru 1805 | . . 3 ⊢ Ⅎ𝑦⊤ | |
2 | nfsbcw.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐴) |
4 | nfsbcw.2 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
5 | 4 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜑) |
6 | 1, 3, 5 | nfsbcdw 3798 | . 2 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝜑) |
7 | 6 | mptru 1547 | 1 ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1541 Ⅎwnf 1784 Ⅎwnfc 2882 [wsbc 3777 |
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 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-tru 1543 df-ex 1781 df-nf 1785 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-sbc 3778 |
This theorem is referenced by: opelopabgf 5540 opelopabf 5545 ralrnmptw 7095 elovmporab 7656 elovmporab1w 7657 ovmpt3rabdm 7669 elovmpt3rab1 7670 dfopab2 8042 dfoprab3s 8043 ralxpes 8127 ralxp3es 8130 frpoins3xpg 8131 frpoins3xp3g 8132 mpoxopoveq 8210 elmptrab 23650 bnj1445 34518 bnj1446 34519 bnj1467 34528 indexa 37064 sdclem1 37074 sbcalf 37445 sbcexf 37446 sbccomieg 41993 rexrabdioph 41994 or2expropbilem2 46201 or2expropbi 46202 ich2exprop 46597 ichnreuop 46598 reuopreuprim 46652 |
Copyright terms: Public domain | W3C validator |