![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 19.41v | Structured version Visualization version GIF version |
Description: Version of 19.41 2229 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1972. (Revised by Rohan Ridenour, 15-Apr-2022.) |
Ref | Expression |
---|---|
19.41v | ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.40 1890 | . . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓)) | |
2 | ax5e 1916 | . . . 4 ⊢ (∃𝑥𝜓 → 𝜓) | |
3 | 2 | anim2i 618 | . . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓)) |
4 | 1, 3 | syl 17 | . 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓)) |
5 | pm3.21 473 | . . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))) | |
6 | 5 | eximdv 1921 | . . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) |
7 | 6 | impcom 409 | . 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) |
8 | 4, 7 | impbii 208 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 ∃wex 1782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 |
This theorem is referenced by: 19.41vv 1955 19.41vvv 1956 19.41vvvv 1957 19.42v 1958 exdistrv 1960 r19.41v 3186 gencbvex 3507 euxfrw 3684 euxfr 3686 euind 3687 dfdif3 4079 zfpair 5381 opabn0 5515 eliunxp 5798 relop 5811 dmuni 5875 dminss 6110 imainss 6111 cnvresima 6187 rnco 6209 coass 6222 xpco 6246 rnoprab 7465 eloprabga 7469 f11o 7884 frxp 8063 omeu 8537 domen 8908 xpassen 9017 dif1enOLD 9113 enfii 9140 ttrclselem2 9669 kmlem3 10095 cflem 10189 genpass 10952 ltexprlem4 10982 hasheqf1oi 14258 elwspths2spth 28954 bnj534 33391 bnj906 33582 bnj908 33583 bnj916 33585 bnj983 33603 bnj986 33607 fmla0 34016 fmlasuc0 34018 dftr6 34363 bj-eeanvw 35207 bj-substw 35216 bj-csbsnlem 35399 bj-clel3gALT 35548 bj-rest10 35588 bj-restuni 35597 bj-imdirco 35690 bj-ccinftydisj 35713 wl-dfclab 36077 eldmqsres2 36777 disjdmqscossss 37294 prter2 37372 dihglb2 39834 prjspeclsp 40979 pm11.6 42746 pm11.71 42751 rfcnnnub 43315 eliunxp2 46483 thinccic 47155 |
Copyright terms: Public domain | W3C validator |