| 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 1988 | . 2 ⊢ (∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐵 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜓))) | |
| 2 | 1 | reeanlem 3239 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: ↔ wb 209 ∧ wa 401 ∈ wcel 2146 ∃wrex 3092 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 |
| This proof depends on definitions: df-bi 210 df-an 402 df-ex 1813 df-ral 3083 df-rex 3093 |
| This theorem is used by: 3reeanv 3241 2reu4lem 4487 disjxiun 5109 fliftfun 7314 poseq 8156 soseq 8157 frrlem9 8293 tfrlem5 8368 uniinqs 8797 eroveu 8812 erovlem 8813 xpf1o 9129 unxpdomlem3 9220 finsschain 9318 dffi3 9393 ttrcltr 9687 rankxplim3 9855 xpnum 9948 kmlem9 10153 sornom 10271 fpwwe2lem11 10636 cnegex 11401 zaddcl 12644 rexanre 15409 o1lo1 15599 o1co 15648 rlimcn3 15652 o1of2 15675 lo1add 15689 lo1mul 15690 summo 15779 ntrivcvgmul 15967 prodmolem2 16000 prodmo 16001 dvds2lem 16336 odd2np1 16409 opoe 16431 omoe 16432 opeo 16433 omeo 16434 bezoutlem4 16610 gcddiv 16619 divgcdcoprmex 16734 pcqmul 16923 pcadd 16959 mul4sq 17024 4sqlem12 17026 prmgaplem7 17127 cyccom 19284 gaorber 19388 psgneu 19586 lsmsubm 19733 pj1eu 19776 efgredlem 19827 efgrelexlemb 19830 qusabl 19945 dprdsubg 20106 dvdsrtr 20461 unitgrp 20476 crngrhmfo 20589 lss1d 21099 lsmspsn 21220 lspsolvlem 21281 lbsextlem2 21298 znfld 21725 cygznlem3 21734 psgnghm 21745 tgcl 23141 restbas 23330 ordtbas2 23363 uncmp 23575 txuni2 23737 txbas 23739 ptbasin 23749 txcnp 23792 txlly 23808 txnlly 23809 tx1stc 23822 tx2ndc 23823 fbasrn 24056 rnelfmlem 24124 fmfnfmlem3 24128 txflf 24178 qustgplem 24293 trust 24401 utoptop 24406 fmucndlem 24462 blin2 24601 metustto 24725 tgqioo 24972 minveclem3b 25602 pmltpc 25624 evthicc2 25634 ovolunlem2 25672 dyaddisj 25770 rolle 26164 dvcvx 26194 itgsubst 26223 plyadd 26389 plymul 26390 coeeu 26397 aalioulem6 26515 dchrptlem2 27444 lgsdchr 27534 mul2sq 27598 2sqlem5 27601 pntibnd 27772 pntlemp 27789 nosupprefixmo 27879 noinfprefixmo 27880 addsproplem2 28178 negsproplem2 28237 mulsuniflem 28357 precsexlem10 28424 zaddscl 28602 zmulscld 28605 zseo 28630 z12addscl 28685 recut 28702 readdscl 28707 remulscl 28710 cgraswap 29146 cgracom 29148 cgratr 29149 flatcgra 29150 dfcgra2 29156 acopyeu 29160 ax5seg 29303 axpasch 29306 axeuclid 29328 axcontlem4 29332 axcontlem9 29337 uhgr2edg 29573 2pthon3v 30307 pjhthmo 31669 superpos 32721 chirredi 32761 cdjreui 32799 cdj3i 32808 xrofsup 33127 archiabllem2c 33528 ccfldextdgrr 34075 ordtconnlem1 34327 dya2iocnrect 34684 txpconn 35736 cvmlift2lem10 35816 cvmlift3lem7 35829 msubco 36035 mclsppslem 36087 altopelaltxp 36480 funtransport 36535 btwnconn1lem13 36603 btwnconn1lem14 36604 segletr 36618 segleantisym 36619 funray 36644 funline 36646 tailfb 36920 mblfinlem3 38342 ismblfin 38344 itg2addnc 38357 ftc1anclem6 38381 heibor1lem 38492 crngohomfo 38689 ispridlc 38753 prter1 39685 hl2at 40211 cdlemn11pre 42016 dihord2pre 42031 dihord4 42064 dihmeetlem20N 42132 mapdpglem32 42511 diophin 43535 diophun 43536 iunrelexpuztr 44477 mullimc 46364 mullimcf 46371 addlimc 46394 fourierdlem42 46895 fourierdlem80 46932 sge0resplit 47152 hoiqssbllem3 47370 |
| Copyright terms: Public domain | W3C validator |