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 2237 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 1956 | . 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑)) | |
2 | exancom 1867 | . 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑)) | |
3 | ancom 464 | . 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑)) | |
4 | 1, 2, 3 | 3bitr4i 306 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 ∃wex 1786 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 |
This theorem is referenced by: exdistr 1961 19.42vv 1964 19.42vvv 1966 4exdistr 1968 2sb5 2279 eeeanv 2352 eu6lem 2574 rexcom4a 3164 cbvrexdva2 3358 ceqsex2 3446 ceqsex2v 3447 reuind 3650 2reu5lem3 3654 sbccomlem 3759 bm1.3ii 5167 eqvinop 5341 dmopabss 5755 dmopab3 5756 dmres 5841 ssrnres 6004 mptpreima 6064 resco 6077 mptfnf 6466 brprcneu 6659 fvprc 6660 fndmin 6816 fliftf 7075 dfoprab2 7220 dmoprab 7263 dmoprabss 7264 fnoprabg 7283 uniuni 7497 zfrep6 7674 opabex3d 7684 opabex3rd 7685 opabex3 7686 fsplit 7831 fsplitOLD 7832 eroveu 8416 rexdif1en 8753 ensymfib 8775 rankuni 9358 aceq1 9610 dfac3 9614 kmlem14 9656 kmlem15 9657 axdc2lem 9941 1idpr 10522 ltexprlem1 10529 ltexprlem4 10532 xpcogend 14416 shftdm 14513 joindm 17722 meetdm 17736 toprntopon 21669 ntreq0 21821 cnextf 22810 adjeu 29816 rexunirn 30406 fpwrelmapffslem 30634 mxidlnzrb 31208 tgoldbachgt 32205 bnj1019 32322 bnj1209 32339 bnj1033 32512 bnj1189 32552 satfdm 32894 dmscut 33638 dfiota3 33855 brimg 33869 funpartlem 33874 bj-eeanvw 34522 bj-snsetex 34765 bj-snglc 34771 bj-bm1.3ii 34847 bj-restuni 34878 bj-xpcossxp 34970 bj-imdirco 34971 itg2addnc 35443 sbccom2lem 35894 eldmres 36020 rnxrn 36136 rp-isfinite6 40663 undmrnresiss 40741 elintima 40791 pm11.58 41530 pm11.71 41537 2sbc5g 41556 iotasbc2 41560 ax6e2nd 41700 ax6e2ndVD 42050 ax6e2ndALT 42072 stoweidlem60 43127 elpglem3 45855 |
Copyright terms: Public domain | W3C validator |