Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 19.21v | Structured version Visualization version GIF version |
Description: Version of 19.21 2075 with a dv condition, requiring fewer axioms.
Notational convention: We sometimes suffix with "v" the label of a theorem using a distinct variable ("dv") condition instead of a non-freeness hypothesis such as Ⅎ𝑥𝜑. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a non-freeness hypothesis ("f" stands for "not free in", see df-nf 1710) instead of a dv condition. For instance, 19.21v 1868 versus 19.21 2075 and vtoclf 3258 versus vtocl 3259. Note that "not free in" is less restrictive than "does not occur in." Note that the version with a dv condition is easily proved from the version with the corresponding non-freeness hypothesis, by using nfv 1843. However, the dv version can often be proved from fewer axioms. (Contributed by NM, 21-Jun-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.) (Proof shortened by Wolf Lammen, 12-Jul-2020.) |
Ref | Expression |
---|---|
19.21v | ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | stdpc5v 1867 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)) | |
2 | ax5e 1841 | . . . 4 ⊢ (∃𝑥𝜑 → 𝜑) | |
3 | 2 | imim1i 63 | . . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)) |
4 | 19.38 1766 | . . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓)) | |
5 | 3, 4 | syl 17 | . 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓)) |
6 | 1, 5 | impbii 199 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∀wal 1481 ∃wex 1704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 |
This theorem depends on definitions: df-bi 197 df-ex 1705 |
This theorem is referenced by: 19.32v 1869 pm11.53v 1906 19.12vvv 1907 pm11.53 2179 19.12vv 2180 cbval2 2279 cbvaldva 2281 sbhb 2438 2sb6 2444 r2al 2939 r3al 2940 r19.21v 2960 ceqsralt 3229 rspc2gv 3321 euind 3393 reu2 3394 reuind 3411 unissb 4469 dfiin2g 4553 axrep5 4776 asymref 5512 fvn0ssdmfun 6350 dff13 6512 mpt22eqb 6769 findcard3 8203 marypha1lem 8339 marypha2lem3 8343 aceq1 8940 kmlem15 8986 cotr2g 13715 bnj864 30992 bnj865 30993 bnj978 31019 bnj1176 31073 bnj1186 31075 dfon2lem8 31695 dffun10 32021 bj-ssb1 32633 bj-ssbcom3lem 32650 bj-cbval2v 32737 bj-axrep5 32792 bj-ralcom4 32868 mpt2bi123f 33971 mptbi12f 33975 elmapintrab 37882 undmrnresiss 37910 dfhe3 38069 dffrege115 38272 ntrneiiso 38389 ntrneikb 38392 pm10.541 38566 pm10.542 38567 19.21vv 38575 pm11.62 38594 2sbc6g 38616 2rexsb 41170 |
Copyright terms: Public domain | W3C validator |