![]() |
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 2202 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1947. (Revised by Rohan Ridenour, 15-Apr-2022.) |
Ref | Expression |
---|---|
19.41v | ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.40 1868 | . . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓)) | |
2 | ax5e 1890 | . . . 4 ⊢ (∃𝑥𝜓 → 𝜓) | |
3 | 2 | anim2i 616 | . . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓)) |
4 | 1, 3 | syl 17 | . 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓)) |
5 | pm3.21 472 | . . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))) | |
6 | 5 | eximdv 1895 | . . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) |
7 | 6 | impcom 408 | . 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) |
8 | 4, 7 | impbii 210 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 ∃wex 1761 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1762 |
This theorem is referenced by: 19.41vv 1928 19.41vvv 1929 19.41vvvv 1930 19.42v 1931 exdistrv 1933 equsexvwOLD 1989 r19.41v 3308 gencbvex 3492 euxfr 3648 euind 3649 dfdif3 4012 zfpair 5213 opabn0 5328 eliunxp 5594 relop 5607 dmuni 5669 dminss 5886 imainss 5887 cnvresima 5962 rnco 5980 coass 5993 xpco 6015 rnoprab 7113 f11o 7504 frxp 7673 omeu 8061 domen 8370 xpassen 8458 kmlem3 9424 cflem 9514 genpass 10277 ltexprlem4 10307 hasheqf1oi 13562 elwspths2spth 27433 bnj534 31627 bnj906 31818 bnj908 31819 bnj916 31821 bnj983 31839 bnj986 31842 fmla0 32237 fmlasuc0 32239 dftr6 32594 bj-eeanvw 33646 bj-csbsnlem 33791 bj-rest10 33978 bj-restuni 33987 bj-ccinftydisj 34053 wl-dfclab 34359 eldmqsres2 35076 prter2 35548 dihglb2 38009 prjspeclsp 38759 pm11.6 40262 pm11.71 40267 rfcnnnub 40832 eliunxp2 43860 |
Copyright terms: Public domain | W3C validator |