![]() |
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 2229 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 1953 | . 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑)) | |
2 | exancom 1864 | . 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑)) | |
3 | ancom 461 | . 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑)) | |
4 | 1, 2, 3 | 3bitr4i 302 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 ∃wex 1781 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 |
This theorem is referenced by: exdistr 1958 19.42vv 1961 19.42vvv 1963 4exdistr 1965 2sb5 2271 eeeanv 2346 eu6lem 2566 rexcom4a 3288 cbvrexdva2OLD 3345 ceqsex2 3526 ceqsex2v 3527 reuind 3745 2reu5lem3 3749 sbccomlem 3860 bm1.3ii 5295 eqvinop 5480 dfid2 5569 dmopabss 5910 dmopab3 5911 dmres 5995 ssrnres 6166 mptpreima 6226 resco 6238 mptfnf 6672 brprcneu 6868 brprcneuALT 6869 fndmin 7031 fliftf 7296 dfoprab2 7451 dmoprab 7494 dmoprabss 7495 fnoprabg 7515 uniuni 7732 zfrep6 7923 opabex3d 7934 opabex3rd 7935 opabex3 7936 fsplit 8085 eroveu 8789 rexdif1enOLD 9142 ensymfib 9170 rankuni 9840 aceq1 10094 dfac3 10098 kmlem14 10140 kmlem15 10141 axdc2lem 10425 1idpr 11006 ltexprlem1 11013 ltexprlem4 11016 xpcogend 14903 shftdm 15000 joindm 18310 meetdm 18324 toprntopon 22356 ntreq0 22510 cnextf 23499 dmscut 27238 adjeu 31005 rexunirn 31595 fpwrelmapffslem 31828 mxidlnzrb 32441 tgoldbachgt 33506 bnj1019 33621 bnj1209 33638 bnj1033 33811 bnj1189 33851 satfdm 34191 dfiota3 34725 brimg 34739 funpartlem 34744 bj-eeanvw 35395 bj-snsetex 35648 bj-snglc 35654 bj-bm1.3ii 35749 bj-dfid2ALT 35750 bj-restuni 35782 bj-xpcossxp 35874 bj-imdirco 35875 itg2addnc 36346 sbccom2lem 36797 eldmres 36943 rnxrn 37073 coss1cnvres 37092 nnoeomeqom 41833 rp-isfinite6 42040 undmrnresiss 42126 elintima 42175 pm11.58 42920 pm11.71 42927 2sbc5g 42946 iotasbc2 42950 ax6e2nd 43090 ax6e2ndVD 43440 ax6e2ndALT 43462 stoweidlem60 44549 mofeu 47162 elpglem3 47406 |
Copyright terms: Public domain | W3C validator |