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 2209 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 1976. (Revised by Rohan Ridenour, 15-Apr-2022.) |
Ref | Expression |
---|---|
19.23v | ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exim 1841 | . . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) | |
2 | ax5e 1920 | . . 3 ⊢ (∃𝑥𝜓 → 𝜓) | |
3 | 1, 2 | syl6 35 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓)) |
4 | ax-5 1918 | . . . 4 ⊢ (𝜓 → ∀𝑥𝜓) | |
5 | 4 | imim2i 16 | . . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)) |
6 | 19.38 1846 | . . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓)) | |
7 | 5, 6 | syl 17 | . 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)) |
8 | 3, 7 | impbii 212 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∀wal 1541 ∃wex 1787 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 |
This theorem depends on definitions: df-bi 210 df-ex 1788 |
This theorem is referenced by: 19.23vv 1951 pm11.53v 1952 equsv 2011 sbequ2OLD 2247 sb4b 2474 sb4bOLD 2475 2mo2 2648 ceqsalv 3440 clel2g 3563 clel4g 3568 elabd2 3576 elabgt 3578 elabg 3582 euind 3634 reuind 3663 sbcg 3771 ralsng 4586 unissb 4850 disjor 5030 dftr2 5160 ssrelrel 5663 cotrg 5973 dffun2 6387 fununi 6452 dff13 7064 dffi2 9036 aceq2 9730 psgnunilem4 18886 metcld 24200 metcld2 24201 isch2 29301 disjorf 30634 funcnv5mpt 30722 bnj1052 32665 bnj1030 32677 dfon2lem8 33482 bj-ssbeq 34568 bj-ssbid2ALT 34578 bj-sblem1 34760 bj-sblem2 34761 bj-sblem 34762 wl-equsalvw 35431 ineleq 36221 cocossss 36294 cossssid3 36322 trcoss2 36337 elmapintrab 40858 elinintrab 40859 undmrnresiss 40886 elintima 40936 relexp0eq 40984 dfhe3 41058 ismnuprim 41583 pm10.52 41654 truniALT 41832 tpid3gVD 42133 truniALTVD 42169 onfrALTVD 42182 unisnALT 42217 |
Copyright terms: Public domain | W3C validator |