Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eeanv | Structured version Visualization version GIF version |
Description: Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.) |
Ref | Expression |
---|---|
eeanv | ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1830 | . 2 ⊢ Ⅎ𝑦𝜑 | |
2 | nfv 1830 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | 1, 2 | eean 2169 | 1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 ∃wex 1695 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-ex 1696 df-nf 1701 |
This theorem is referenced by: eeeanv 2171 ee4anv 2172 2mo2 2538 cgsex2g 3212 cgsex4g 3213 vtocl2 3234 spc2egv 3268 dtru 4783 copsex2t 4883 copsex2g 4884 xpnz 5472 fununi 5878 wfrlem4 7305 wfrfun 7312 tfrlem7 7366 ener 7888 enerOLD 7889 domtr 7895 unen 7925 undom 7933 sbthlem10 7964 mapen 8009 infxpenc2 8728 fseqen 8733 dfac5lem4 8832 zorn2lem6 9206 fpwwe2lem12 9342 genpnnp 9706 hashfacen 13095 summo 14295 ntrivcvgmul 14473 prodmo 14505 iscatd2 16165 gictr 17540 gsumval3eu 18128 ptbasin 21190 txcls 21217 txbasval 21219 hmphtr 21396 reconn 22439 phtpcer 22602 phtpcerOLD 22603 pcohtpy 22628 mbfi1flimlem 23295 mbfmullem 23298 itg2add 23332 spc2ed 28696 brabgaf 28800 pconcon 30467 txscon 30477 frrlem4 31027 frrlem5c 31030 neibastop1 31524 bj-dtru 31985 riscer 32957 fnchoice 38211 fzisoeu 38455 stoweidlem35 38928 |
Copyright terms: Public domain | W3C validator |