| 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 3238 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: ↔ wb 209 ∧ wa 401 ∈ wcel 2146 ∃wrex 3091 |
| 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 3082 df-rex 3092 |
| This theorem is used by: 3reeanv 3240 2reu4lem 4486 disjxiun 5108 fliftfun 7319 poseq 8160 soseq 8161 frrlem9 8297 tfrlem5 8372 uniinqs 8801 eroveu 8816 erovlem 8817 xpf1o 9134 unxpdomlem3 9225 finsschain 9323 dffi3 9398 ttrcltr 9692 rankxplim3 9860 xpnum 9953 kmlem9 10158 sornom 10276 fpwwe2lem11 10645 cnegex 11410 zaddcl 12653 rexanre 15426 o1lo1 15616 o1co 15665 rlimcn3 15669 o1of2 15692 lo1add 15706 lo1mul 15707 summo 15795 ntrivcvgmul 15983 prodmolem2 16016 prodmo 16017 dvds2lem 16352 odd2np1 16425 opoe 16447 omoe 16448 opeo 16449 omeo 16450 bezoutlem4 16626 gcddiv 16635 divgcdcoprmex 16750 pcqmul 16939 pcadd 16975 mul4sq 17040 4sqlem12 17042 prmgaplem7 17143 cyccom 19322 gaorber 19426 psgneu 19624 lsmsubm 19771 pj1eu 19814 efgredlem 19865 efgrelexlemb 19868 qusabl 19983 dprdsubg 20144 dvdsrtr 20500 unitgrp 20515 crngrhmfo 20628 lss1d 21138 lsmspsn 21259 lspsolvlem 21320 lbsextlem2 21337 znfld 21764 cygznlem3 21773 psgnghm 21784 tgcl 23180 restbas 23369 ordtbas2 23402 uncmp 23614 txuni2 23777 txbas 23779 ptbasin 23789 txcnp 23832 txlly 23848 txnlly 23849 tx1stc 23862 tx2ndc 23863 fbasrn 24096 rnelfmlem 24164 fmfnfmlem3 24168 txflf 24218 qustgplem 24333 trust 24441 utoptop 24446 fmucndlem 24502 blin2 24641 metustto 24765 tgqioo 25012 minveclem3b 25642 pmltpc 25664 evthicc2 25674 ovolunlem2 25712 dyaddisj 25810 rolle 26204 dvcvx 26234 itgsubst 26263 plyadd 26429 plymul 26430 coeeu 26437 aalioulem6 26555 dchrptlem2 27484 lgsdchr 27574 mul2sq 27638 2sqlem5 27641 pntibnd 27812 pntlemp 27829 nosupprefixmo 27919 noinfprefixmo 27920 addsproplem2 28218 negsproplem2 28277 mulsuniflem 28397 precsexlem10 28464 zaddscl 28642 zmulscld 28645 zseo 28670 z12addscl 28725 recut 28742 readdscl 28747 remulscl 28750 cgraswap 29186 cgracom 29188 cgratr 29189 flatcgra 29190 dfcgra2 29196 acopyeu 29200 ax5seg 29347 axpasch 29350 axeuclid 29372 axcontlem4 29376 axcontlem9 29381 uhgr2edg 29620 2pthon3v 30363 pjhthmo 31729 superpos 32781 chirredi 32821 cdjreui 32859 cdj3i 32868 xrofsup 33186 archiabllem2c 33583 ccfldextdgrr 34130 ordtconnlem1 34382 dya2iocnrect 34740 txpconn 35765 cvmlift2lem10 35845 cvmlift3lem7 35858 msubco 36064 mclsppslem 36116 altopelaltxp 36509 funtransport 36564 btwnconn1lem13 36632 btwnconn1lem14 36633 segletr 36647 segleantisym 36648 funray 36673 funline 36675 tailfb 36949 mblfinlem3 38371 ismblfin 38373 itg2addnc 38386 ftc1anclem6 38410 heibor1lem 38522 crngohomfo 38719 ispridlc 38783 prter1 39715 hl2at 40241 cdlemn11pre 42046 dihord2pre 42061 dihord4 42094 dihmeetlem20N 42162 mapdpglem32 42541 diophin 43580 diophun 43581 iunrelexpuztr 44522 mullimc 46409 mullimcf 46416 addlimc 46439 fourierdlem42 46940 fourierdlem80 46977 sge0resplit 47197 hoiqssbllem3 47415 |
| Copyright terms: Public domain | W3C validator |