![]() |
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 1945. Version of r19.41 3250 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 3060 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))) | |
2 | anass 467 | . . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))) | |
3 | 2 | exbii 1842 | . 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))) |
4 | 19.41v 1945 | . . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓)) | |
5 | df-rex 3060 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
6 | 5 | bicomi 223 | . . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑) |
7 | 4, 6 | bianbi 625 | . 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) |
8 | 1, 3, 7 | 3bitr2i 298 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 394 ∃wex 1773 ∈ wcel 2098 ∃wrex 3059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-rex 3060 |
This theorem is referenced by: r19.42v 3180 r19.41vv 3214 3reeanv 3217 reuxfr1d 3742 reuind 3745 iuncom4 5005 dfiun2gOLD 5035 iunxiun 5101 inuni 5346 xpiundi 5748 xpiundir 5749 imaco 6257 coiun 6262 abrexco 7254 imaiun 7255 isomin 7344 isoini 7345 imaeqsexv 7370 imaeqexov 7659 oarec 8583 mapsnend 9061 unfi 9197 brttrcl2 9739 genpass 11034 4fvwrd4 13656 4sqlem12 16928 imasleval 17526 lsmspsn 20981 utoptop 24183 metrest 24477 metust 24511 cfilucfil 24512 metuel2 24518 sleadd1 27952 addsuniflem 27964 addsasslem1 27966 addsasslem2 27967 addsdilem1 28101 0reno 28297 renegscl 28298 readdscl 28299 remulscl 28302 istrkg2ld 28336 axsegcon 28810 fusgreg2wsp 30218 nmoo0 30673 nmop0 31868 nmfn0 31869 rexunirn 32368 dmrab 32373 iunrnmptss 32435 ressupprn 32552 ordtconnlem1 33656 dya2icoseg2 34029 dya2iocnei 34033 omssubaddlem 34050 omssubadd 34051 satfvsuclem2 35101 satf0 35113 satffunlem1lem2 35144 satffunlem2lem2 35147 bj-mpomptALT 36729 mptsnunlem 36948 fvineqsneq 37022 rabiun 37197 iundif1 37198 poimir 37257 ismblfin 37265 eldmqs1cossres 38261 erimeq2 38280 prter2 38483 prter3 38484 islshpat 38619 lshpsmreu 38711 islpln5 39138 islvol5 39182 cdlemftr3 40168 dvhb1dimN 40589 dib1dim 40768 mapdpglem3 41278 hdmapglem7a 41530 diophrex 42337 dfsclnbgr6 47330 r19.41dv 48060 |
Copyright terms: Public domain | W3C validator |