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 303 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 ∃wex 1782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 |
This theorem is referenced by: exdistr 1958 19.42vv 1961 19.42vvv 1963 4exdistr 1965 2sb5 2272 eeeanv 2348 eu6lem 2573 rexcom4a 3236 cbvrexdva2 3393 ceqsex2 3482 ceqsex2v 3483 reuind 3688 2reu5lem3 3692 sbccomlem 3803 bm1.3ii 5226 eqvinop 5401 dfid2 5491 dmopabss 5827 dmopab3 5828 dmres 5913 ssrnres 6081 mptpreima 6141 resco 6154 mptfnf 6568 brprcneu 6764 brprcneuALT 6765 fndmin 6922 fliftf 7186 dfoprab2 7333 dmoprab 7376 dmoprabss 7377 fnoprabg 7397 uniuni 7612 zfrep6 7797 opabex3d 7808 opabex3rd 7809 opabex3 7810 fsplit 7957 fsplitOLD 7958 eroveu 8601 rexdif1en 8944 ensymfib 8970 rankuni 9621 aceq1 9873 dfac3 9877 kmlem14 9919 kmlem15 9920 axdc2lem 10204 1idpr 10785 ltexprlem1 10792 ltexprlem4 10795 xpcogend 14685 shftdm 14782 joindm 18093 meetdm 18107 toprntopon 22074 ntreq0 22228 cnextf 23217 adjeu 30251 rexunirn 30840 fpwrelmapffslem 31067 mxidlnzrb 31644 tgoldbachgt 32643 bnj1019 32759 bnj1209 32776 bnj1033 32949 bnj1189 32989 satfdm 33331 dmscut 34005 dfiota3 34225 brimg 34239 funpartlem 34244 bj-eeanvw 34895 bj-snsetex 35153 bj-snglc 35159 bj-bm1.3ii 35235 bj-dfid2ALT 35236 bj-restuni 35268 bj-xpcossxp 35360 bj-imdirco 35361 itg2addnc 35831 sbccom2lem 36282 eldmres 36408 rnxrn 36524 rp-isfinite6 41125 undmrnresiss 41212 elintima 41261 pm11.58 42008 pm11.71 42015 2sbc5g 42034 iotasbc2 42038 ax6e2nd 42178 ax6e2ndVD 42528 ax6e2ndALT 42550 stoweidlem60 43601 mofeu 46175 elpglem3 46418 |
Copyright terms: Public domain | W3C validator |