![]() |
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 1908. Version of r19.41 3283 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 461 | . . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))) | |
2 | 1 | exbii 1810 | . . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))) |
3 | 19.41v 1908 | . . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓)) | |
4 | 2, 3 | bitr3i 269 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓)) |
5 | df-rex 3088 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))) | |
6 | df-rex 3088 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
7 | 6 | anbi1i 614 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓)) |
8 | 4, 5, 7 | 3bitr4i 295 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 387 ∃wex 1742 ∈ wcel 2048 ∃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: r19.41vv 3284 r19.42v 3285 3reeanv 3303 reuxfr4d 3648 reuind 3649 iuncom4 4794 dfiun2g 4819 dfiun2gOLD 4820 iunxiun 4879 inuni 5096 reuxfrd 5168 xpiundi 5465 xpiundir 5466 imaco 5937 coiun 5942 abrexco 6822 imaiun 6823 isomin 6907 isoini 6908 oarec 7981 mapsnend 8377 genpass 10221 4fvwrd4 12836 4sqlem12 16138 imasleval 16660 lsmspsn 19568 utoptop 22536 metrest 22827 metust 22861 cfilucfil 22862 metuel2 22868 istrkg2ld 25938 axsegcon 26406 fusgreg2wsp 27860 nmoo0 28335 nmop0 29534 nmfn0 29535 rexunirn 30027 dmrab 30029 iunrnmptss 30076 ordtconnlem1 30768 dya2icoseg2 31138 dya2iocnei 31142 omssubaddlem 31159 omssubadd 31160 bj-mpt2mptALT 33855 mptsnunlem 33996 fvineqsneq 34069 rabiun 34254 iundif1 34255 poimir 34314 ismblfin 34322 eldmqs1cossres 35286 erim2 35304 prter2 35410 prter3 35411 islshpat 35546 lshpsmreu 35638 islpln5 36064 islvol5 36108 cdlemftr3 37094 dvhb1dimN 37515 dib1dim 37694 mapdpglem3 38204 hdmapglem7a 38456 diophrex 38713 |
Copyright terms: Public domain | W3C validator |