New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > sbie | GIF version |
Description: Conversion of implicit substitution to explicit substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) |
Ref | Expression |
---|---|
sbie.1 | ⊢ Ⅎxψ |
sbie.2 | ⊢ (x = y → (φ ↔ ψ)) |
Ref | Expression |
---|---|
sbie | ⊢ ([y / x]φ ↔ ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nftru 1554 | . . 3 ⊢ Ⅎx ⊤ | |
2 | sbie.1 | . . . 4 ⊢ Ⅎxψ | |
3 | 2 | a1i 10 | . . 3 ⊢ ( ⊤ → Ⅎxψ) |
4 | sbie.2 | . . . 4 ⊢ (x = y → (φ ↔ ψ)) | |
5 | 4 | a1i 10 | . . 3 ⊢ ( ⊤ → (x = y → (φ ↔ ψ))) |
6 | 1, 3, 5 | sbied 2036 | . 2 ⊢ ( ⊤ → ([y / x]φ ↔ ψ)) |
7 | 6 | trud 1323 | 1 ⊢ ([y / x]φ ↔ ψ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 176 ⊤ wtru 1316 Ⅎwnf 1544 [wsb 1648 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 |
This theorem depends on definitions: df-bi 177 df-an 360 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 |
This theorem is referenced by: equsb3lem 2101 elsb3 2103 elsb4 2104 cbveu 2224 mo4f 2236 2mos 2283 bm1.1 2338 eqsb3lem 2453 clelsb3 2455 cbvab 2471 cbvralf 2829 cbvreu 2833 sbralie 2848 cbvrab 2857 reu2 3024 sbcco2 3069 sbcie2g 3079 sbcel2gv 3106 sbcralt 3118 sbcralg 3120 sbcrexg 3121 sbcreug 3122 sbcel12g 3151 sbceqg 3152 cbvralcsf 3198 cbvreucsf 3200 cbvrabcsf 3201 sbss 3659 cbviota 4344 cbvopab1 4632 sbcbrg 4685 cbvmpt 5676 fvfullfunlem1 5861 |
Copyright terms: Public domain | W3C validator |