| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > r19.42v | Structured version Visualization version GIF version | ||
| Description: Restricted quantifier version of 19.42v 1953 (see also 19.42 2236). (Contributed by NM, 27-May-1998.) |
| Ref | Expression |
|---|---|
| r19.42v | ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | r19.41v 3189 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑)) | |
| 2 | ancom 460 | . . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑)) | |
| 3 | 2 | rexbii 3094 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑)) |
| 4 | ancom 460 | . 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑)) | |
| 5 | 1, 3, 4 | 3bitr4i 303 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wrex 3070 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-rex 3071 |
| This theorem is referenced by: rexcomOLD 3291 ceqsrexbv 3656 ceqsrex2v 3658 2reuswap 3752 2reuswap2 3753 2reu5 3764 2rmoswap 3767 dfiun2g 5030 iunrab 5052 iunin2 5071 iundif2 5074 reusv2lem4 5401 iunopab 5564 iunopabOLD 5565 cnvuni 5897 elidinxp 6062 xpdifid 6188 dfpo2 6316 elunirn 7271 f1oiso 7371 oprabrexex2 8003 oeeu 8641 trcl 9768 dfac5lem2 10164 axgroth4 10872 rexuz2 12941 4fvwrd4 13688 cshwsexaOLD 14863 divalglem10 16439 divalgb 16441 lsmelval2 21084 tgcmp 23409 hauscmplem 23414 unisngl 23535 xkobval 23594 txtube 23648 txcmplem1 23649 txkgen 23660 xkococnlem 23667 mbfaddlem 25695 mbfsup 25699 elaa 26358 dchrisumlem3 27535 elold 27908 0reno 28429 colperpexlem3 28740 midex 28745 iscgra1 28818 ax5seg 28953 edglnl 29160 usgr2pth0 29785 hhcmpl 31219 sumdmdii 32434 reuxfrdf 32510 unipreima 32653 fpwrelmapffslem 32743 elirng 33736 esumfsup 34071 reprdifc 34642 bnj168 34744 bnj1398 35048 cvmliftlem15 35303 ellines 36153 bj-elsngl 36969 bj-dfmpoa 37119 ptrecube 37627 cnambfre 37675 islshpat 39018 lfl1dim 39122 glbconxN 39380 3dim0 39459 2dim 39472 1dimN 39473 islpln5 39537 islvol5 39581 dalem20 39695 lhpex2leN 40015 mapdval4N 41634 rexrabdioph 42805 rmxdioph 43028 expdiophlem1 43033 imaiun1 43664 coiun1 43665 ismnuprim 44313 prmunb2 44330 fourierdlem48 46169 2reuimp0 47126 2reuimp 47127 wtgoldbnnsum4prm 47789 bgoldbnnsum3prm 47791 dfvopnbgr2 47839 stgredgiun 47925 islindeps2 48400 isldepslvec2 48402 sepnsepolem1 48819 |
| Copyright terms: Public domain | W3C validator |