![]() |
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 2224 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 1964. (Revised by Rohan Ridenour, 15-Apr-2022.) |
Ref | Expression |
---|---|
19.41v | ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.40 1882 | . . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓)) | |
2 | ax5e 1908 | . . . 4 ⊢ (∃𝑥𝜓 → 𝜓) | |
3 | 2 | anim2i 615 | . . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∃𝑥𝜑 ∧ 𝜓)) |
4 | 1, 3 | syl 17 | . 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓)) |
5 | pm3.21 470 | . . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))) | |
6 | 5 | eximdv 1913 | . . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) |
7 | 6 | impcom 406 | . 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) |
8 | 4, 7 | impbii 208 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 394 ∃wex 1774 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 |
This theorem is referenced by: 19.41vv 1947 19.41vvv 1948 19.41vvvv 1949 19.42v 1950 exdistrv 1952 r19.41v 3179 gencbvex 3527 euxfrw 3715 euxfr 3717 euind 3718 dfdif3 4113 zfpair 5425 opabn0 5559 eliunxp 5844 relop 5857 dmuni 5921 dminss 6164 imainss 6165 cnvresima 6241 rnco 6263 coass 6276 xpco 6300 rnoprab 7529 eloprabga 7533 f11o 7960 frxp 8140 omeu 8615 domen 8992 xpassen 9104 dif1enOLD 9200 enfii 9223 ttrclselem2 9769 kmlem3 10195 cflem 10289 genpass 11052 ltexprlem4 11082 hasheqf1oi 14368 elwspths2spth 29901 bnj534 34584 bnj906 34775 bnj908 34776 bnj916 34778 bnj983 34796 bnj986 34800 fmla0 35210 fmlasuc0 35212 rexxfr3dALT 35467 dftr6 35573 bj-eeanvw 36418 bj-substw 36427 bj-csbsnlem 36609 bj-clel3gALT 36755 bj-rest10 36795 bj-restuni 36804 bj-imdirco 36897 bj-ccinftydisj 36920 wl-dfclab 37291 eldmqsres2 37986 disjdmqscossss 38501 prter2 38579 dihglb2 41041 prjspeclsp 42266 pm11.6 44066 pm11.71 44071 rfcnnnub 44635 eliunxp2 47712 thinccic 48382 |
Copyright terms: Public domain | W3C validator |