| 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 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.) |
| Ref | Expression |
|---|---|
| nfsbcw.1 | ⊢ Ⅎ𝑥𝐴 |
| nfsbcw.2 | ⊢ Ⅎ𝑥𝜑 |
| Ref | Expression |
|---|---|
| nfsbcw | ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nftru 1804 | . . 3 ⊢ Ⅎ𝑦⊤ | |
| 2 | nfsbcw.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
| 3 | 2 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐴) |
| 4 | nfsbcw.2 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
| 5 | 4 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜑) |
| 6 | 1, 3, 5 | nfsbcdw 3809 | . 2 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝜑) |
| 7 | 6 | mptru 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 |