![]() |
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 | nfv 2013 | . 2 ⊢ Ⅎ𝑦𝜑 | |
2 | nfv 2013 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | 1, 2 | reean 3316 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 386 ∃wrex 3118 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-10 2192 ax-11 2207 ax-12 2220 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-ral 3122 df-rex 3123 |
This theorem is referenced by: 3reeanv 3318 2ralor 3319 disjxiun 4872 fliftfun 6822 tfrlem5 7747 uniinqs 8097 eroveu 8113 erovlem 8114 xpf1o 8397 unxpdomlem3 8441 unfi 8502 finsschain 8548 dffi3 8612 rankxplim3 9028 xpnum 9097 kmlem9 9302 sornom 9421 fpwwe2lem12 9785 cnegex 10543 zaddcl 11752 rexanre 14470 o1lo1 14652 o1co 14701 rlimcn2 14705 o1of2 14727 lo1add 14741 lo1mul 14742 summo 14832 ntrivcvgmul 15014 prodmolem2 15045 prodmo 15046 dvds2lem 15378 odd2np1 15446 opoe 15468 omoe 15469 opeo 15470 omeo 15471 bezoutlem4 15639 gcddiv 15648 divgcdcoprmex 15759 pcqmul 15936 pcadd 15971 mul4sq 16036 4sqlem12 16038 prmgaplem7 16139 gaorber 18098 psgneu 18284 lsmsubm 18426 pj1eu 18467 efgredlem 18519 efgredlemOLD 18520 efgrelexlemb 18523 qusabl 18628 cygabl 18652 dprdsubg 18784 dvdsrtr 19013 unitgrp 19028 lss1d 19329 lsmspsn 19450 lspsolvlem 19509 lbsextlem2 19527 znfld 20275 cygznlem3 20284 psgnghm 20292 tgcl 21151 restbas 21340 ordtbas2 21373 uncmp 21584 txuni2 21746 txbas 21748 ptbasin 21758 txcnp 21801 txlly 21817 txnlly 21818 tx1stc 21831 tx2ndc 21832 fbasrn 22065 rnelfmlem 22133 fmfnfmlem3 22137 txflf 22187 qustgplem 22301 trust 22410 utoptop 22415 fmucndlem 22472 blin2 22611 metustto 22735 tgqioo 22980 minveclem3b 23603 pmltpc 23623 evthicc2 23633 ovolunlem2 23671 dyaddisj 23769 rolle 24159 dvcvx 24189 itgsubst 24218 plyadd 24379 plymul 24380 coeeu 24387 aalioulem6 24498 dchrptlem2 25410 lgsdchr 25500 mul2sq 25564 2sqlem5 25567 pntibnd 25702 pntlemp 25719 cgraswap 26136 cgracom 26138 cgratr 26139 dfcgra2 26145 acopyeu 26150 ax5seg 26244 axpasch 26247 axeuclid 26269 axcontlem4 26273 axcontlem9 26278 uhgr2edg 26511 2pthon3v 27279 pjhthmo 28712 superpos 29764 chirredi 29804 cdjreui 29842 cdj3i 29851 xrofsup 30076 archiabllem2c 30290 ordtconnlem1 30511 dya2iocnrect 30884 txpconn 31756 cvmlift2lem10 31836 cvmlift3lem7 31849 msubco 31970 mclsppslem 32022 poseq 32287 soseq 32288 noprefixmo 32382 altopelaltxp 32617 funtransport 32672 btwnconn1lem13 32740 btwnconn1lem14 32741 segletr 32755 segleantisym 32756 funray 32781 funline 32783 tailfb 32905 mblfinlem3 33991 ismblfin 33993 itg2addnc 34006 ftc1anclem6 34032 heibor1lem 34149 crngohomfo 34346 ispridlc 34410 prter1 34953 hl2at 35479 cdlemn11pre 37284 dihord2pre 37299 dihord4 37332 dihmeetlem20N 37400 mapdpglem32 37779 diophin 38179 diophun 38180 iunrelexpuztr 38851 mullimc 40641 mullimcf 40648 addlimc 40673 fourierdlem42 41158 fourierdlem80 41195 sge0resplit 41412 hoiqssbllem3 41630 2reu4a 42012 |
Copyright terms: Public domain | W3C validator |