![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > rexeqdv | Unicode version |
Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007.) |
Ref | Expression |
---|---|
raleq1d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
rexeqdv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleq1d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | rexeq 2869 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 16 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem is referenced by: rexeqbidv 2881 rexeqbidva 2883 fnunirn 5962 oarec 6768 fival 7379 marypha1lem 7400 marypha1 7401 wemapwe 7614 zornn0g 8345 supcvg 12594 vdwlem6 13313 rami 13342 imasleval 13725 isssc 13979 ipodrsfi 14548 grppropd 14782 sylow1lem2 15192 sylow3lem1 15220 lsmass 15261 pj1fval 15285 efgrelexlema 15340 ablfacrplem 15582 pgpfac1lem2 15592 pgpfac1lem3 15594 pgpfac1lem4 15595 ablfac2 15606 dvdsrval 15709 dvdsrpropd 15760 znunit 16803 cnpfval 17256 cmpcov 17410 cmpsublem 17420 cmpsub 17421 tgcmp 17422 uncmp 17424 hauscmplem 17427 1stcfb 17465 2ndcctbss 17475 1stcelcls 17481 llyi 17494 nllyi 17495 cldllycmp 17515 ptrescn 17628 isufl 17902 fmid 17949 alexsublem 18032 alexsubb 18034 alexsubALTlem4 18038 alexsubALT 18039 cnextfres 18056 tsmsf1o 18131 utopval 18219 imasf1oxms 18476 bndth 18940 ovolicc2 19375 ellimc2 19721 limcflf 19725 plyval 20069 aannenlem1 20202 aannenlem2 20203 ulm2 20258 nb3graprlem2 21418 fargshiftfo 21582 isplig 21722 isgrp2d 21780 isgrpda 21842 pjhth 22852 pjhfval 22855 pjhtheu2 22875 ballotlemfc0 24707 ballotlemfcc 24708 ispcon 24867 zprod 25220 br8 25331 br6 25332 br4 25333 brsegle 25950 hilbert1.1 25996 limsucncmpi 26103 volsupnfl 26154 isdrngo2 26468 isnacs 26652 eldioph 26710 islssfg 27040 ellspd 27126 itgoval 27238 stoweidlem50 27670 stoweidlem57 27677 frgra2v 28107 lcvfbr 29507 lkrlspeqN 29658 pointsetN 30227 dia1dim2 31549 dib1dim2 31655 diclspsn 31681 dih1dimatlem 31816 lcfrvalsnN 32028 mapdpglem3 32162 mapdpglem26 32185 mapdpglem27 32186 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2389 |
This theorem depends on definitions: df-bi 178 df-an 361 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-cleq 2401 df-clel 2404 df-nfc 2533 df-rex 2676 |
Copyright terms: Public domain | W3C validator |