![]() |
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 2192 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 nonfreeness hypothesis such as Ⅎ𝑥𝜑. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a nonfreeness hypothesis ("f" stands for "not free in", see df-nf 1778) instead of a disjoint variable condition. For instance, 19.21v 1934 versus 19.21 2192 and vtoclf 3544 versus vtocl 3538. 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 nonfreeness hypothesis, by using nfv 1909. 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 1933 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)) | |
2 | ax5e 1907 | . . . 4 ⊢ (∃𝑥𝜑 → 𝜑) | |
3 | 2 | imim1i 63 | . . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)) |
4 | 19.38 1833 | . . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓)) | |
5 | 3, 4 | syl 17 | . 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓)) |
6 | 1, 5 | impbii 208 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1531 ∃wex 1773 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 |
This theorem depends on definitions: df-bi 206 df-ex 1774 |
This theorem is referenced by: 19.32v 1935 pm11.53v 1939 19.12vvv 1984 cbvaldvaw 2033 2sb6 2081 sbrimvw 2086 sbal 2151 hbsbw 2161 sbrim 2292 pm11.53 2334 19.12vv 2335 sbhb 2512 r19.21vOLD 3172 r2al 3186 r3al 3188 ralcom4 3275 ralcom4OLD 3276 nfra2wOLD 3289 cbvraldva2 3336 ceqsralt 3499 rspc2gv 3613 elabgt 3654 euind 3712 reu2 3713 reuind 3741 unissb 4933 unissbOLD 4934 dfiin2g 5025 axrep5 5281 asymref 6107 fvn0ssdmfun 7066 dff13 7246 mpo2eqb 7533 xpord3inddlem 8134 findcard3 9280 findcard3OLD 9281 marypha1lem 9423 marypha2lem3 9427 aceq1 10107 kmlem15 10154 cotr2g 14919 bnj864 34388 bnj865 34389 bnj978 34415 bnj1176 34471 bnj1186 34473 dfon2lem8 35223 dffun10 35347 mpobi123f 37486 mptbi12f 37490 sn-axrep5v 41492 unielss 42422 elmapintrab 42782 undmrnresiss 42810 dfhe3 42981 dffrege115 43184 ntrneiiso 43297 ntrneikb 43300 pm10.541 43581 pm10.542 43582 19.21vv 43590 pm11.62 43608 2sbc6g 43629 2rexsb 46260 |
Copyright terms: Public domain | W3C validator |