New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 19.21v | GIF version |
Description: Special case of Theorem 19.21 of [Margaris] p. 90. Notational convention: We sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as Ⅎxφ in 19.21 1796 via the use of distinct variable conditions combined with nfv 1619. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the distinct variable condition; e.g. euf 2210 derived from df-eu 2208. The "f" stands for "not free in" which is less restrictive than "does not occur in." (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
19.21v | ⊢ (∀x(φ → ψ) ↔ (φ → ∀xψ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1619 | . 2 ⊢ Ⅎxφ | |
2 | 1 | 19.21 1796 | 1 ⊢ (∀x(φ → ψ) ↔ (φ → ∀xψ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 176 ∀wal 1540 |
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-11 1746 |
This theorem depends on definitions: df-bi 177 df-ex 1542 df-nf 1545 |
This theorem is referenced by: pm11.53 1893 19.12vv 1898 sbhb 2107 2sb6 2113 sbcom2 2114 2sb6rf 2118 2exsb 2132 r3al 2671 ceqsralt 2882 euind 3023 reu2 3024 reuind 3039 unissb 3921 dfiin2g 4000 ssfin 4470 spfininduct 4540 dff13 5471 spacind 6287 |
Copyright terms: Public domain | W3C validator |