Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 19.23v | Structured version Visualization version GIF version |
Description: Version of 19.23 2067 with a dv condition instead of a non-freeness hypothesis. (Contributed by NM, 28-Jun-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020.) |
Ref | Expression |
---|---|
19.23v | ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exim 1751 | . . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) | |
2 | 19.9v 1883 | . . 3 ⊢ (∃𝑥𝜓 ↔ 𝜓) | |
3 | 1, 2 | syl6ib 240 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓)) |
4 | ax-5 1827 | . . . 4 ⊢ (𝜓 → ∀𝑥𝜓) | |
5 | 4 | imim2i 16 | . . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)) |
6 | 19.38 1757 | . . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓)) | |
7 | 5, 6 | syl 17 | . 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)) |
8 | 3, 7 | impbii 198 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∀wal 1473 ∃wex 1695 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 |
This theorem depends on definitions: df-bi 196 df-ex 1696 |
This theorem is referenced by: 19.23vv 1890 pm11.53v 1893 equsalvw 1918 2mo2 2538 euind 3360 reuind 3378 unissb 4405 disjor 4567 dftr2 4682 ssrelrel 5143 cotrg 5426 dffun2 5814 fununi 5878 dff13 6416 dffi2 8212 aceq2 8825 psgnunilem4 17740 metcld 22912 metcld2 22913 isch2 27464 disjorf 28774 funcnv5mpt 28852 bnj1052 30297 bnj1030 30309 dfon2lem8 30939 bj-ssbeq 31816 bj-ssb0 31817 bj-ssb1a 31821 bj-ssb1 31822 bj-ssbequ2 31832 bj-ssbid2ALT 31835 elmapintrab 36901 elinintrab 36902 undmrnresiss 36929 elintima 36964 relexp0eq 37012 dfhe3 37089 pm10.52 37586 truniALT 37772 tpid3gVD 38099 truniALTVD 38136 onfrALTVD 38149 unisnALT 38184 |
Copyright terms: Public domain | W3C validator |