![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reeanv | Structured version Visualization version Unicode version |
Description: Rearrange restricted existential quantifiers. (Contributed by NM, 9-May-1999.) |
Ref | Expression |
---|---|
reeanv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1761 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfv 1761 |
. 2
![]() ![]() ![]() ![]() | |
3 | 1, 2 | reean 2957 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1664 df-nf 1668 df-ral 2742 df-rex 2743 |
This theorem is referenced by: 3reeanv 2959 2ralor 2960 disjxiun 4399 fliftfun 6205 tfrlem5 7098 uniinqs 7443 eroveu 7458 erovlem 7459 xpf1o 7734 unxpdomlem3 7778 unfi 7838 finsschain 7881 dffi3 7945 rankxplim3 8352 xpnum 8385 kmlem9 8588 sornom 8707 fpwwe2lem12 9066 cnegex 9814 zaddcl 10977 rexanre 13409 o1lo1 13601 o1co 13650 rlimcn2 13654 o1of2 13676 lo1add 13690 lo1mul 13691 summo 13783 ntrivcvgmul 13958 prodmolem2 13989 prodmo 13990 dvds2lem 14315 odd2np1 14365 bezoutlem4OLD 14506 bezoutlem4 14509 gcddiv 14517 opoe 14761 omoe 14762 opeo 14763 omeo 14764 pcqmul 14803 pcadd 14834 mul4sq 14898 4sqlem12 14900 prmgaplem7 15027 gaorber 16962 psgneu 17147 lsmsubm 17305 pj1eu 17346 efgredlem 17397 efgrelexlemb 17400 qusabl 17503 cygabl 17525 dprdsubg 17657 dvdsrtr 17880 unitgrp 17895 lss1d 18186 lsmspsn 18307 lspsolvlem 18365 lbsextlem2 18382 znfld 19131 cygznlem3 19140 psgnghm 19148 tgcl 19985 restbas 20174 ordtbas2 20207 uncmp 20418 txuni2 20580 txbas 20582 ptbasin 20592 txcnp 20635 txlly 20651 txnlly 20652 tx1stc 20665 tx2ndc 20666 fbasrn 20899 rnelfmlem 20967 fmfnfmlem3 20971 txflf 21021 qustgplem 21135 trust 21244 utoptop 21249 fmucndlem 21306 blin2 21444 metustto 21568 tgqioo 21818 minveclem3b 22370 minveclem3bOLD 22382 pmltpc 22401 evthicc2 22411 ovolunlem2 22451 dyaddisj 22554 rolle 22942 dvcvx 22972 itgsubst 23001 plyadd 23171 plymul 23172 coeeu 23179 aalioulem6 23293 dchrptlem2 24193 lgsdchr 24276 mul2sq 24293 2sqlem5 24296 pntibnd 24431 pntlemp 24448 cgraswap 24862 cgracom 24864 cgratr 24865 dfcgra2 24871 acopyeu 24875 ax5seg 24968 axpasch 24971 axeuclid 24993 axcontlem4 24997 axcontlem9 25002 usgra2edg 25109 frgrawopreglem5 25776 pjhthmo 26955 superpos 28007 chirredi 28047 cdjreui 28085 cdj3i 28094 xrofsup 28353 archiabllem2c 28512 ordtconlem1 28730 dya2iocnrect 29103 txpcon 29955 cvmlift2lem10 30035 cvmlift3lem7 30048 msubco 30169 mclsppslem 30221 ghomgrpilem2 30304 poseq 30491 soseq 30492 altopelaltxp 30743 funtransport 30798 btwnconn1lem13 30866 btwnconn1lem14 30867 segletr 30881 segleantisym 30882 funray 30907 funline 30909 tailfb 31033 mblfinlem3 31979 ismblfin 31981 itg2addnc 31996 ftc1anclem6 32022 heibor1lem 32141 crngohomfo 32239 ispridlc 32303 prter1 32451 hl2at 32970 cdlemn11pre 34778 dihord2pre 34793 dihord4 34826 dihmeetlem20N 34894 mapdpglem32 35273 diophin 35615 diophun 35616 iunrelexpuztr 36311 mullimc 37696 mullimcf 37703 addlimc 37729 fourierdlem42 38012 fourierdlem42OLD 38013 fourierdlem80 38050 sge0resplit 38248 hoiqssbllem3 38446 2reu4a 38610 usgr2edg 39291 |
Copyright terms: Public domain | W3C validator |