Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reeanv | Structured version Visualization version GIF version |
Description: Rearrange restricted existential quantifiers. (Contributed by NM, 9-May-1999.) |
Ref | Expression |
---|---|
reeanv | ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exdistrv 1947 | . 2 ⊢ (∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐵 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜓))) | |
2 | 1 | reeanlem 3363 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 ∈ wcel 2105 ∃wrex 3136 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-ral 3140 df-rex 3141 |
This theorem is referenced by: 3reeanv 3366 2ralor 3367 2reu4lem 4461 disjxiun 5054 fliftfun 7054 tfrlem5 8005 uniinqs 8366 eroveu 8381 erovlem 8382 xpf1o 8667 unxpdomlem3 8712 unfi 8773 finsschain 8819 dffi3 8883 rankxplim3 9298 xpnum 9368 kmlem9 9572 sornom 9687 fpwwe2lem12 10051 cnegex 10809 zaddcl 12010 rexanre 14694 o1lo1 14882 o1co 14931 rlimcn2 14935 o1of2 14957 lo1add 14971 lo1mul 14972 summo 15062 ntrivcvgmul 15246 prodmolem2 15277 prodmo 15278 dvds2lem 15610 odd2np1 15678 opoe 15700 omoe 15701 opeo 15702 omeo 15703 bezoutlem4 15878 gcddiv 15887 divgcdcoprmex 15998 pcqmul 16178 pcadd 16213 mul4sq 16278 4sqlem12 16280 prmgaplem7 16381 cyccom 18284 gaorber 18376 psgneu 18563 lsmsubm 18707 pj1eu 18751 efgredlem 18802 efgrelexlemb 18805 qusabl 18914 cygablOLD 18940 dprdsubg 19075 dvdsrtr 19331 unitgrp 19346 lss1d 19664 lsmspsn 19785 lspsolvlem 19843 lbsextlem2 19860 znfld 20635 cygznlem3 20644 psgnghm 20652 tgcl 21505 restbas 21694 ordtbas2 21727 uncmp 21939 txuni2 22101 txbas 22103 ptbasin 22113 txcnp 22156 txlly 22172 txnlly 22173 tx1stc 22186 tx2ndc 22187 fbasrn 22420 rnelfmlem 22488 fmfnfmlem3 22492 txflf 22542 qustgplem 22656 trust 22765 utoptop 22770 fmucndlem 22827 blin2 22966 metustto 23090 tgqioo 23335 minveclem3b 23958 pmltpc 23978 evthicc2 23988 ovolunlem2 24026 dyaddisj 24124 rolle 24514 dvcvx 24544 itgsubst 24573 plyadd 24734 plymul 24735 coeeu 24742 aalioulem6 24853 dchrptlem2 25768 lgsdchr 25858 mul2sq 25922 2sqlem5 25925 pntibnd 26096 pntlemp 26113 cgraswap 26533 cgracom 26535 cgratr 26536 flatcgra 26537 dfcgra2 26543 acopyeu 26547 ax5seg 26651 axpasch 26654 axeuclid 26676 axcontlem4 26680 axcontlem9 26685 uhgr2edg 26917 2pthon3v 27649 pjhthmo 29006 superpos 30058 chirredi 30098 cdjreui 30136 cdj3i 30145 xrofsup 30418 archiabllem2c 30751 ccfldextdgrr 30956 ordtconnlem1 31066 dya2iocnrect 31438 txpconn 32376 cvmlift2lem10 32456 cvmlift3lem7 32469 msubco 32675 mclsppslem 32727 poseq 32992 soseq 32993 frrlem9 33028 noprefixmo 33099 altopelaltxp 33334 funtransport 33389 btwnconn1lem13 33457 btwnconn1lem14 33458 segletr 33472 segleantisym 33473 funray 33498 funline 33500 tailfb 33622 mblfinlem3 34812 ismblfin 34814 itg2addnc 34827 ftc1anclem6 34853 heibor1lem 34968 crngohomfo 35165 ispridlc 35229 prter1 35895 hl2at 36421 cdlemn11pre 38226 dihord2pre 38241 dihord4 38274 dihmeetlem20N 38342 mapdpglem32 38721 diophin 39247 diophun 39248 iunrelexpuztr 39942 mullimc 41773 mullimcf 41780 addlimc 41805 fourierdlem42 42311 fourierdlem80 42348 sge0resplit 42565 hoiqssbllem3 42783 |
Copyright terms: Public domain | W3C validator |