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 1905 (see also 19.42 2092). (Contributed by NM, 27-May-1998.) |
Ref | Expression |
---|---|
r19.42v | ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.41v 3070 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑)) | |
2 | ancom 465 | . . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑)) | |
3 | 2 | rexbii 3023 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑)) |
4 | ancom 465 | . 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑)) | |
5 | 1, 3, 4 | 3bitr4i 291 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 ∃wrex 2897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-rex 2902 |
This theorem is referenced by: ceqsrexbv 3307 ceqsrex2v 3308 2reuswap 3377 2reu5 3383 rabasiun 4459 iunrab 4503 iunin2 4520 iundif2 4523 reusv2lem4 4798 iunopab 4936 elxp2OLD 5057 cnvuni 5231 xpdifid 5481 elunirn 6413 f1oiso 6501 oprabrexex2 7049 oeeu 7570 trcl 8487 dfac5lem2 8830 axgroth4 9533 rexuz2 11615 4fvwrd4 12328 cshwsexa 13421 divalglem10 14963 divalgb 14965 lsmelval2 18906 tgcmp 21014 hauscmplem 21019 unisngl 21140 xkobval 21199 txtube 21253 txcmplem1 21254 txkgen 21265 xkococnlem 21272 mbfaddlem 23233 mbfsup 23237 elaa 23875 dchrisumlem3 24980 colperpexlem3 25424 midex 25429 iscgra1 25502 ax5seg 25618 usg2spot2nb 26592 usgreg2spot 26594 sumdmdii 28658 2reuswap2 28712 unipreima 28826 fpwrelmapffslem 28895 esumfsup 29459 bnj168 30052 bnj1398 30356 cvmliftlem15 30534 dfpo2 30898 ellines 31429 bj-elsngl 32149 bj-dfmpt2a 32252 ptrecube 32579 cnambfre 32628 islshpat 33322 lfl1dim 33426 glbconxN 33682 3dim0 33761 2dim 33774 1dimN 33775 islpln5 33839 islvol5 33883 dalem20 33997 lhpex2leN 34317 mapdval4N 35939 rexrabdioph 36376 rmxdioph 36601 expdiophlem1 36606 imaiun1 36962 coiun1 36963 prmunb2 37532 fourierdlem48 39047 2rmoswap 39833 wtgoldbnnsum4prm 40218 bgoldbnnsum3prm 40220 usgr2pth0 40971 fusgr2wsp2nb 41498 islindeps2 42066 isldepslvec2 42068 |
Copyright terms: Public domain | W3C validator |