Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > r19.41v | Structured version Visualization version GIF version |
Description: Restricted quantifier version 19.41v 1941. Version of r19.41 3345 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 17-Dec-2003.) Reduce dependencies on axioms. (Revised by BJ, 29-Mar-2020.) |
Ref | Expression |
---|---|
r19.41v | ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anass 469 | . . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))) | |
2 | 1 | exbii 1839 | . . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))) |
3 | 19.41v 1941 | . . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓)) | |
4 | 2, 3 | bitr3i 278 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓)) |
5 | df-rex 3141 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))) | |
6 | df-rex 3141 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
7 | 6 | anbi1i 623 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓)) |
8 | 4, 5, 7 | 3bitr4i 304 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 ∃wex 1771 ∈ wcel 2105 ∃wrex 3136 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-rex 3141 |
This theorem is referenced by: r19.41vv 3346 r19.42v 3347 3reeanv 3366 reuxfr1d 3738 reuind 3741 iuncom4 4918 dfiun2g 4946 dfiun2gOLD 4947 iunxiun 5010 inuni 5237 xpiundi 5615 xpiundir 5616 imaco 6097 coiun 6102 abrexco 6994 imaiun 6995 isomin 7079 isoini 7080 oarec 8177 mapsnend 8576 genpass 10419 4fvwrd4 13015 4sqlem12 16280 imasleval 16802 lsmspsn 19785 utoptop 22770 metrest 23061 metust 23095 cfilucfil 23096 metuel2 23102 istrkg2ld 26173 axsegcon 26640 fusgreg2wsp 28042 nmoo0 28495 nmop0 29690 nmfn0 29691 rexunirn 30183 dmrab 30187 iunrnmptss 30245 ordtconnlem1 31066 dya2icoseg2 31435 dya2iocnei 31439 omssubaddlem 31456 omssubadd 31457 satfvsuclem2 32504 satf0 32516 satffunlem1lem2 32547 satffunlem2lem2 32550 bj-mpomptALT 34303 mptsnunlem 34501 fvineqsneq 34575 rabiun 34746 iundif1 34747 poimir 34806 ismblfin 34814 eldmqs1cossres 35773 erim2 35791 prter2 35897 prter3 35898 islshpat 36033 lshpsmreu 36125 islpln5 36551 islvol5 36595 cdlemftr3 37581 dvhb1dimN 38002 dib1dim 38181 mapdpglem3 38691 hdmapglem7a 38943 diophrex 39250 |
Copyright terms: Public domain | W3C validator |