![]() |
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 2191 with a disjoint variable 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 1828) instead of a disjoint variable condition. For instance, 19.21v 1982 versus 19.21 2191 and vtoclf 3458 versus vtocl 3459. Note that "not free in" is less restrictive than "does not occur in". Note that the version with a disjoint variable condition is easily proved from the version with the corresponding non-freeness hypothesis, by using nfv 1957. 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 1981 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)) | |
2 | ax5e 1955 | . . . 4 ⊢ (∃𝑥𝜑 → 𝜑) | |
3 | 2 | imim1i 63 | . . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)) |
4 | 19.38 1882 | . . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓)) | |
5 | 3, 4 | syl 17 | . 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓)) |
6 | 1, 5 | impbii 201 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∀wal 1599 ∃wex 1823 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 |
This theorem depends on definitions: df-bi 199 df-ex 1824 |
This theorem is referenced by: 19.32v 1983 pm11.53v 1987 19.12vvv 2037 2sb6 2252 pm11.53 2314 19.12vv 2315 cbval2 2373 cbvaldva 2375 sbhb 2517 r2al 3120 r3al 3121 r19.21v 3141 ceqsralt 3430 rspc2gv 3522 euind 3604 reu2 3605 reuind 3627 unissb 4704 dfiin2g 4786 axrep5 5012 asymref 5767 fvn0ssdmfun 6614 dff13 6784 mpt22eqb 7046 findcard3 8491 marypha1lem 8627 marypha2lem3 8631 aceq1 9273 kmlem15 9321 cotr2g 14124 bnj864 31605 bnj865 31606 bnj978 31632 bnj1176 31686 bnj1186 31688 dfon2lem8 32297 dffun10 32624 bj-ssb1 33238 bj-ssbcom3lem 33254 bj-cbval2v 33336 bj-axrep5 33383 bj-ralcom4 33452 wl-dfralv 33985 mpt2bi123f 34587 mptbi12f 34591 elmapintrab 38831 undmrnresiss 38859 dfhe3 39017 dffrege115 39220 ntrneiiso 39337 ntrneikb 39340 pm10.541 39514 pm10.542 39515 19.21vv 39523 pm11.62 39542 2sbc6g 39563 2rexsb 42121 |
Copyright terms: Public domain | W3C validator |