| 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 1949. Version of r19.41 3263 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 | df-rex 3071 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))) | |
| 2 | anass 468 | . . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))) | |
| 3 | 2 | exbii 1848 | . 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))) |
| 4 | 19.41v 1949 | . . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓)) | |
| 5 | df-rex 3071 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
| 6 | 5 | bicomi 224 | . . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑) |
| 7 | 4, 6 | bianbi 627 | . 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) |
| 8 | 1, 3, 7 | 3bitr2i 299 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1779 ∈ wcel 2108 ∃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: r19.42v 3191 r19.41vv 3227 3reeanv 3230 reuxfr1d 3756 reuind 3759 iuncom4 5000 dfiun2gOLD 5031 iunxiun 5097 inuni 5350 xpiundi 5756 xpiundir 5757 imaco 6271 coiun 6276 abrexco 7264 imaiun 7265 isomin 7357 isoini 7358 imaeqsexvOLD 7383 imaeqexov 7671 oarec 8600 mapsnend 9076 unfi 9211 brttrcl2 9754 genpass 11049 4fvwrd4 13688 4sqlem12 16994 imasleval 17586 lsmspsn 21083 utoptop 24243 metrest 24537 metust 24571 cfilucfil 24572 metuel2 24578 sleadd1 28022 addsuniflem 28034 addsasslem1 28036 addsasslem2 28037 addsdilem1 28177 0reno 28429 renegscl 28430 readdscl 28431 remulscl 28434 istrkg2ld 28468 axsegcon 28942 fusgreg2wsp 30355 nmoo0 30810 nmop0 32005 nmfn0 32006 rexunirn 32511 dmrab 32516 iunrnmptss 32578 ressupprn 32699 ordtconnlem1 33923 dya2icoseg2 34280 dya2iocnei 34284 omssubaddlem 34301 omssubadd 34302 satfvsuclem2 35365 satf0 35377 satffunlem1lem2 35408 satffunlem2lem2 35411 rexxfr3dALT 35644 bj-mpomptALT 37120 mptsnunlem 37339 fvineqsneq 37413 rabiun 37600 iundif1 37601 poimir 37660 ismblfin 37668 eldmqs1cossres 38660 erimeq2 38679 prter2 38882 prter3 38883 islshpat 39018 lshpsmreu 39110 islpln5 39537 islvol5 39581 cdlemftr3 40567 dvhb1dimN 40988 dib1dim 41167 mapdpglem3 41677 hdmapglem7a 41929 diophrex 42786 dfsclnbgr6 47844 r19.41dv 48722 reuxfr1dd 48726 |
| Copyright terms: Public domain | W3C validator |