![]() |
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 1949 (see also 19.42 2224). (Contributed by NM, 27-May-1998.) |
Ref | Expression |
---|---|
r19.42v | ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.41v 3186 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑)) | |
2 | ancom 459 | . . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑)) | |
3 | 2 | rexbii 3091 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑)) |
4 | ancom 459 | . 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑)) | |
5 | 1, 3, 4 | 3bitr4i 302 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 394 ∃wrex 3067 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-rex 3068 |
This theorem is referenced by: rexcomOLD 3286 ceqsrexbv 3644 ceqsrex2v 3646 2reuswap 3743 2reuswap2 3744 2reu5 3755 2rmoswap 3758 dfiun2g 5037 iunrab 5059 iunin2 5078 iundif2 5081 reusv2lem4 5405 iunopab 5565 iunopabOLD 5566 cnvuni 5893 elidinxp 6052 xpdifid 6177 dfpo2 6305 elunirn 7267 f1oiso 7365 oprabrexex2 7988 oeeu 8630 trcl 9759 dfac5lem2 10155 axgroth4 10863 rexuz2 12921 4fvwrd4 13661 cshwsexaOLD 14815 divalglem10 16386 divalgb 16388 lsmelval2 20977 tgcmp 23325 hauscmplem 23330 unisngl 23451 xkobval 23510 txtube 23564 txcmplem1 23565 txkgen 23576 xkococnlem 23583 mbfaddlem 25609 mbfsup 25613 elaa 26271 dchrisumlem3 27444 elold 27816 0reno 28245 colperpexlem3 28556 midex 28561 iscgra1 28634 ax5seg 28769 edglnl 28976 usgr2pth0 29599 hhcmpl 31030 sumdmdii 32245 reuxfrdf 32310 unipreima 32451 fpwrelmapffslem 32535 elirng 33397 esumfsup 33722 reprdifc 34292 bnj168 34394 bnj1398 34698 cvmliftlem15 34941 ellines 35781 bj-elsngl 36480 bj-dfmpoa 36630 ptrecube 37126 cnambfre 37174 islshpat 38521 lfl1dim 38625 glbconxN 38883 3dim0 38962 2dim 38975 1dimN 38976 islpln5 39040 islvol5 39084 dalem20 39198 lhpex2leN 39518 mapdval4N 41137 rexrabdioph 42245 rmxdioph 42468 expdiophlem1 42473 imaiun1 43112 coiun1 43113 ismnuprim 43762 prmunb2 43779 fourierdlem48 45571 2reuimp0 46523 2reuimp 46524 wtgoldbnnsum4prm 47171 bgoldbnnsum3prm 47173 dfvopnbgr2 47217 islindeps2 47629 isldepslvec2 47631 sepnsepolem1 48018 |
Copyright terms: Public domain | W3C validator |