![]() |
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 1912 (see also 19.42 2169). (Contributed by NM, 27-May-1998.) |
Ref | Expression |
---|---|
r19.42v | ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.41v 3282 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑)) | |
2 | ancom 453 | . . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑)) | |
3 | 2 | rexbii 3188 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑)) |
4 | ancom 453 | . 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑)) | |
5 | 1, 3, 4 | 3bitr4i 295 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 387 ∃wrex 3083 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-rex 3088 |
This theorem is referenced by: rexcom 3290 ceqsrexbv 3558 ceqsrex2v 3559 2reuswap 3643 2reuswap2 3644 2reu5 3652 2rmoswap 3655 iunrab 4838 iunin2 4855 iundif2 4858 reusv2lem4 5151 iunopab 5294 cnvuni 5603 elidinxp 5753 xpdifid 5862 elunirn 6833 f1oiso 6925 oprabrexex2 7489 oeeu 8028 trcl 8962 dfac5lem2 9342 axgroth4 10050 rexuz2 12111 4fvwrd4 12841 cshwsexa 14046 divalglem10 15611 divalgb 15613 lsmelval2 19591 tgcmp 21725 hauscmplem 21730 unisngl 21851 xkobval 21910 txtube 21964 txcmplem1 21965 txkgen 21976 xkococnlem 21983 mbfaddlem 23976 mbfsup 23980 elaa 24620 dchrisumlem3 25781 colperpexlem3 26232 midex 26237 iscgra1 26310 ax5seg 26439 edglnl 26643 usgr2pth0 27266 hhcmpl 28768 sumdmdii 29985 unipreima 30167 fpwrelmapffslem 30241 esumfsup 31002 reprdifc 31575 bnj168 31677 bnj1398 31980 cvmliftlem15 32159 dfpo2 32540 ellines 33163 bj-elsngl 33827 bj-dfmpoa 33948 ptrecube 34362 cnambfre 34410 islshpat 35627 lfl1dim 35731 glbconxN 35988 3dim0 36067 2dim 36080 1dimN 36081 islpln5 36145 islvol5 36189 dalem20 36303 lhpex2leN 36623 mapdval4N 38242 rexrabdioph 38816 rmxdioph 39038 expdiophlem1 39043 imaiun1 39388 coiun1 39389 ismnuprim 40034 prmunb2 40088 fourierdlem48 41895 2reuimp0 42744 2reuimp 42745 wtgoldbnnsum4prm 43360 bgoldbnnsum3prm 43362 islindeps2 43930 isldepslvec2 43932 |
Copyright terms: Public domain | W3C validator |