![]() |
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 1954. Version of r19.41 3245 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 470 | . . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))) | |
2 | 1 | exbii 1851 | . . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))) |
3 | 19.41v 1954 | . . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓)) | |
4 | 2, 3 | bitr3i 277 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓)) |
5 | df-rex 3071 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))) | |
6 | df-rex 3071 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
7 | 6 | anbi1i 625 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓)) |
8 | 4, 5, 7 | 3bitr4i 303 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 ∃wex 1782 ∈ wcel 2107 ∃wrex 3070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-rex 3071 |
This theorem is referenced by: r19.42v 3184 r19.41vv 3214 3reeanv 3217 reuxfr1d 3709 reuind 3712 iuncom4 4963 dfiun2gOLD 4992 iunxiun 5058 inuni 5301 xpiundi 5703 xpiundir 5704 imaco 6204 coiun 6209 abrexco 7192 imaiun 7193 isomin 7283 isoini 7284 imaeqsexv 7309 imaeqexov 7593 oarec 8510 mapsnend 8983 unfi 9119 brttrcl2 9655 genpass 10950 4fvwrd4 13567 4sqlem12 16833 imasleval 17428 lsmspsn 20560 utoptop 23602 metrest 23896 metust 23930 cfilucfil 23931 metuel2 23937 sleadd1 27320 addsunif 27332 addsasslem1 27333 addsasslem2 27334 istrkg2ld 27444 axsegcon 27918 fusgreg2wsp 29322 nmoo0 29775 nmop0 30970 nmfn0 30971 rexunirn 31463 dmrab 31468 iunrnmptss 31530 ressupprn 31651 ordtconnlem1 32562 dya2icoseg2 32935 dya2iocnei 32939 omssubaddlem 32956 omssubadd 32957 satfvsuclem2 34011 satf0 34023 satffunlem1lem2 34054 satffunlem2lem2 34057 bj-mpomptALT 35636 mptsnunlem 35855 fvineqsneq 35929 rabiun 36097 iundif1 36098 poimir 36157 ismblfin 36165 eldmqs1cossres 37167 erimeq2 37186 prter2 37389 prter3 37390 islshpat 37525 lshpsmreu 37617 islpln5 38044 islvol5 38088 cdlemftr3 39074 dvhb1dimN 39495 dib1dim 39674 mapdpglem3 40184 hdmapglem7a 40436 diophrex 41141 r19.41dv 46973 |
Copyright terms: Public domain | W3C validator |