Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 19.42v | Structured version Visualization version GIF version |
Description: Version of 19.42 2238 with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
19.42v | ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.41v 1950 | . 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑)) | |
2 | exancom 1861 | . 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑)) | |
3 | ancom 463 | . 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑)) | |
4 | 1, 2, 3 | 3bitr4i 305 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 ∃wex 1780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 |
This theorem is referenced by: exdistr 1955 19.42vv 1958 19.42vvv 1960 19.42vvvOLD 1961 4exdistr 1963 2sb5 2282 eeeanv 2371 eu6lem 2658 rexcom4 3249 rexcom4a 3251 cbvrexdva2 3457 ceqsex2 3543 ceqsex2v 3544 reuind 3744 2reu5lem3 3748 sbccomlem 3853 bm1.3ii 5206 eqvinop 5378 dmopabss 5787 dmopab3 5788 dmres 5875 ssrnres 6035 mptpreima 6092 resco 6103 mptfnf 6483 brprcneu 6662 fndmin 6815 fliftf 7068 dfoprab2 7212 dmoprab 7255 dmoprabss 7256 fnoprabg 7275 uniuni 7484 zfrep6 7656 opabex3d 7666 opabex3rd 7667 opabex3 7668 fsplit 7812 fsplitOLD 7813 eroveu 8392 rankuni 9292 aceq1 9543 dfac3 9547 kmlem14 9589 kmlem15 9590 axdc2lem 9870 1idpr 10451 ltexprlem1 10458 ltexprlem4 10461 xpcogend 14334 shftdm 14430 joindm 17613 meetdm 17627 toprntopon 21533 ntreq0 21685 cnextf 22674 adjeu 29666 rexunirn 30256 fpwrelmapffslem 30468 mxidlnzrb 30981 tgoldbachgt 31934 bnj1019 32051 bnj1209 32068 bnj1033 32241 bnj1189 32281 satfdm 32616 dmscut 33272 dfiota3 33384 brimg 33398 funpartlem 33403 bj-eeanvw 34047 bj-snsetex 34278 bj-snglc 34284 bj-bm1.3ii 34360 bj-restuni 34391 itg2addnc 34961 sbccom2lem 35417 eldmres 35545 rnxrn 35661 rp-isfinite6 39904 undmrnresiss 39984 elintima 40018 pm11.58 40742 pm11.71 40749 2sbc5g 40768 iotasbc2 40772 ax6e2nd 40912 ax6e2ndVD 41262 ax6e2ndALT 41284 stoweidlem60 42365 elpglem3 44835 |
Copyright terms: Public domain | W3C validator |