![]() |
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 2204 with a disjoint variable condition instead of a nonfreeness hypothesis. (Contributed by NM, 28-Jun-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020.) Remove dependency on ax-6 1971. (Revised by Rohan Ridenour, 15-Apr-2022.) |
Ref | Expression |
---|---|
19.23v | ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exim 1836 | . . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) | |
2 | ax5e 1915 | . . 3 ⊢ (∃𝑥𝜓 → 𝜓) | |
3 | 1, 2 | syl6 35 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓)) |
4 | ax-5 1913 | . . . 4 ⊢ (𝜓 → ∀𝑥𝜓) | |
5 | 4 | imim2i 16 | . . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)) |
6 | 19.38 1841 | . . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓)) | |
7 | 5, 6 | syl 17 | . 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)) |
8 | 3, 7 | impbii 208 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1539 ∃wex 1781 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 |
This theorem depends on definitions: df-bi 206 df-ex 1782 |
This theorem is referenced by: 19.23vv 1946 pm11.53v 1947 equsv 2006 sb4b 2473 sb4bOLD 2474 2mo2 2647 ceqsalv 3480 clel2g 3608 clel4g 3613 elabd2 3621 elabgt 3623 elabg 3627 euind 3681 reuind 3710 sbcg 3817 ralsng 4633 snssb 4742 unissb 4899 unissbOLD 4900 disjor 5084 dftr2 5223 ssrelrel 5751 cotrg 6060 cotrgOLD 6061 cotrgOLDOLD 6062 dffun2OLDOLD 6506 fununi 6574 dff13 7199 dffi2 9356 aceq2 10052 psgnunilem4 19275 metcld 24666 metcld2 24667 isch2 30063 disjorf 31395 funcnv5mpt 31482 bnj1052 33478 bnj1030 33490 dfon2lem8 34257 bj-ssbeq 35106 bj-ssbid2ALT 35116 bj-sblem1 35297 bj-sblem2 35298 bj-sblem 35299 wl-equsalvw 35986 ineleq 36804 cocossss 36887 cossssid3 36920 trcoss2 36935 elmapintrab 41828 elinintrab 41829 undmrnresiss 41856 elintima 41905 relexp0eq 41953 dfhe3 42027 ismnuprim 42554 pm10.52 42625 truniALT 42803 tpid3gVD 43104 truniALTVD 43140 onfrALTVD 43153 unisnALT 43188 |
Copyright terms: Public domain | W3C validator |