| 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 2235 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1967. (Revised by Rohan Ridenour, 15-Apr-2022.) |
| Ref | Expression |
|---|---|
| 19.41v | ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 19.40 1886 | . . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓)) | |
| 2 | ax5e 1912 | . . . 4 ⊢ (∃𝑥𝜓 → 𝜓) | |
| 3 | 2 | anim2i 617 | . . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓)) |
| 4 | 1, 3 | syl 17 | . 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓)) |
| 5 | pm3.21 471 | . . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))) | |
| 6 | 5 | eximdv 1917 | . . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) |
| 7 | 6 | impcom 407 | . 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) |
| 8 | 4, 7 | impbii 209 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1779 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 |
| This theorem is referenced by: 19.41vv 1950 19.41vvv 1951 19.41vvvv 1952 19.42v 1953 exdistrv 1955 r19.41v 3189 gencbvex 3541 euxfrw 3727 euxfr 3729 euind 3730 dfdif3OLD 4118 zfpair 5421 opabn0 5558 eliunxp 5848 relop 5861 dmuni 5925 dminss 6173 imainss 6174 cnvresima 6250 rnco 6272 coass 6285 xpco 6309 rnoprab 7538 eloprabga 7542 f11o 7971 frxp 8151 omeu 8623 domen 9002 xpassen 9106 dif1enOLD 9202 enfii 9226 ttrclselem2 9766 kmlem3 10193 cflem 10285 cflemOLD 10286 genpass 11049 ltexprlem4 11079 hasheqf1oi 14390 elwspths2spth 29987 bnj534 34753 bnj906 34944 bnj908 34945 bnj916 34947 bnj983 34965 bnj986 34969 fmla0 35387 fmlasuc0 35389 rexxfr3dALT 35644 dftr6 35751 bj-eeanvw 36714 bj-substw 36723 bj-csbsnlem 36904 bj-clel3gALT 37049 bj-rest10 37089 bj-restuni 37098 bj-imdirco 37191 bj-ccinftydisj 37214 wl-dfclab 37597 eldmqsres2 38289 disjdmqscossss 38804 prter2 38882 dihglb2 41344 prjspeclsp 42622 pm11.6 44411 pm11.71 44416 rfcnnnub 45041 eliunxp2 48250 thinccic 49118 |
| Copyright terms: Public domain | W3C validator |