![]() |
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 1954 and 19.42v 1958. For a version with fewer disjoint variable conditions but requiring more axioms, see eeanv 2346. (Contributed by BJ, 30-Sep-2022.) |
Ref | Expression |
---|---|
exdistrv | ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exdistr 1959 | . 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) | |
2 | 19.41v 1954 | . 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) | |
3 | 1, 2 | bitri 275 | 1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 ∃wex 1782 |
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 |
This theorem is referenced by: 4exdistrv 1961 eu6lem 2572 2mo2 2648 reeanv 3220 cgsex2g 3492 cgsex4g 3493 cgsex4gOLD 3494 spc2egv 3561 spc2ed 3563 dtruALT2 5330 exexneq 5396 dtruOLD 5403 copsex2t 5454 copsex2gOLD 5456 xpnz 6116 fununi 6581 frrlem4 8225 wfrlem4OLD 8263 wfrfunOLD 8270 tfrlem7 8334 ener 8948 domtr 8954 unen 8997 undom 9010 undomOLD 9011 sbthlem10 9043 mapen 9092 entrfil 9139 domtrfil 9146 sbthfilem 9152 infxpenc2 9965 fseqen 9970 dfac5lem4 10069 zorn2lem6 10444 fpwwe2lem11 10584 genpnnp 10948 hashfacen 14358 hashfacenOLD 14359 summo 15609 ntrivcvgmul 15794 prodmo 15826 iscatd2 17568 catcone0 17574 gictr 19072 gsumval3eu 19688 ptbasin 22944 txcls 22971 txbasval 22973 hmphtr 23150 reconn 24207 phtpcer 24374 pcohtpy 24399 mbfi1flimlem 25103 mbfmullem 25106 itg2add 25140 brabgaf 31569 pconnconn 33865 txsconn 33875 neibastop1 34860 bj-unexg 35538 copsex2d 35639 riscer 36476 disjecxrn 36880 br1cosscnvxrn 36965 rictr 40731 fnchoice 43308 fzisoeu 43608 stoweidlem35 44350 elsprel 45741 |
Copyright terms: Public domain | W3C validator |