| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > exdistrv | Structured version Visualization version GIF version | ||
| Description: Distribute a pair of existential quantifiers (over disjoint variables) over a conjunction. Combination of 19.41v 1949 and 19.42v 1953. For a version with fewer disjoint variable conditions but requiring more axioms, see eeanv 2351. (Contributed by BJ, 30-Sep-2022.) |
| Ref | Expression |
|---|---|
| exdistrv | ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exdistr 1954 | . 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) | |
| 2 | 19.41v 1949 | . 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) | |
| 3 | 1, 2 | bitri 275 | 1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1779 |
| 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 |
| This theorem is referenced by: 4exdistrv 1956 eu6lem 2573 2mo2 2647 reeanv 3229 cgsex2g 3527 cgsex4g 3528 cgsex4gOLD 3529 spc2egv 3599 spc2ed 3601 dtruALT2 5370 exexneq 5439 dtruOLD 5446 copsex2t 5497 xpnz 6179 fununi 6641 frrlem4 8314 wfrlem4OLD 8352 wfrfunOLD 8359 tfrlem7 8423 ener 9041 domtr 9047 unen 9086 undom 9099 undomOLD 9100 sbthlem10 9132 mapen 9181 entrfil 9225 domtrfil 9232 sbthfilem 9238 infxpenc2 10062 fseqen 10067 dfac5lem4 10166 dfac5lem4OLD 10168 zorn2lem6 10541 fpwwe2lem11 10681 genpnnp 11045 hashfacen 14493 summo 15753 ntrivcvgmul 15938 prodmo 15972 iscatd2 17724 catcone0 17730 gictr 19294 gsumval3eu 19922 ptbasin 23585 txcls 23612 txbasval 23614 hmphtr 23791 reconn 24850 phtpcer 25027 pcohtpy 25053 mbfi1flimlem 25757 mbfmullem 25760 itg2add 25794 brabgaf 32620 pconnconn 35236 txsconn 35246 neibastop1 36360 bj-unexg 37039 copsex2d 37140 riscer 37995 disjecxrn 38390 br1cosscnvxrn 38475 rictr 42530 fnchoice 45034 fzisoeu 45312 stoweidlem35 46050 elsprel 47462 grictr 47892 |
| Copyright terms: Public domain | W3C validator |