|   | 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 2235 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 1948 | . 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑)) | |
| 2 | exancom 1860 | . 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑)) | |
| 3 | ancom 460 | . 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑)) | |
| 4 | 1, 2, 3 | 3bitr4i 303 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1778 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 | 
| This theorem is referenced by: exdistr 1953 19.42vv 1956 19.42vvv 1958 4exdistr 1960 2sb5 2277 eeeanv 2351 eu6lem 2572 r3ex 3197 rexcom4a 3291 cbvrexdva2OLD 3349 ceqsex2 3534 ceqsex2v 3535 reuind 3758 2reu5lem3 3762 sbccomlemOLD 3869 bm1.3iiOLD 5301 eqvinop 5491 dfid2 5579 dmopabss 5928 dmopab3 5929 dmxp 5938 rnopabss 5965 rnopab3 5966 dmres 6029 ssrnres 6197 mptpreima 6257 resco 6269 mptfnf 6702 brprcneu 6895 brprcneuALT 6896 fndmin 7064 fliftf 7336 dfoprab2 7492 dmoprab 7537 dmoprabss 7538 fnoprabg 7557 uniuni 7783 zfrep6 7980 opabex3d 7991 opabex3rd 7992 opabex3 7993 fsplit 8143 eroveu 8853 rexdif1enOLD 9200 ensymfib 9225 rankuni 9904 aceq1 10158 dfac3 10162 kmlem14 10205 kmlem15 10206 axdc2lem 10489 1idpr 11070 ltexprlem1 11077 ltexprlem4 11080 xpcogend 15014 shftdm 15111 joindm 18421 meetdm 18435 toprntopon 22932 ntreq0 23086 cnextf 24075 dmscut 27857 adjeu 31909 rexunirn 32512 fpwrelmapffslem 32744 mxidlnzrb 33509 tgoldbachgt 34679 bnj1019 34794 bnj1209 34811 bnj1033 34984 bnj1189 35024 satfdm 35375 dfiota3 35925 brimg 35939 funpartlem 35944 bj-eeanvw 36715 bj-snsetex 36965 bj-snglc 36971 bj-bm1.3ii 37066 bj-dfid2ALT 37067 bj-restuni 37099 bj-xpcossxp 37191 bj-imdirco 37192 itg2addnc 37682 sbccom2lem 38132 eldmres 38272 rnxrn 38400 coss1cnvres 38419 nnoeomeqom 43330 rp-isfinite6 43536 undmrnresiss 43622 elintima 43671 pm11.58 44414 pm11.71 44421 2sbc5g 44440 iotasbc2 44444 ax6e2nd 44583 ax6e2ndVD 44933 ax6e2ndALT 44955 modelaxreplem3 45002 stoweidlem60 46080 coxp 48749 mofeu 48762 elpglem3 49287 | 
| Copyright terms: Public domain | W3C validator |