![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexlimdvw | Structured version Visualization version Unicode version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Jun-2014.) |
Ref | Expression |
---|---|
rexlimdvw.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
rexlimdvw |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimdvw.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1d 26 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | rexlimdv 2877 |
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 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1664 df-ral 2742 df-rex 2743 |
This theorem is referenced by: odi 7280 omeulem1 7283 qsss 7424 findcard3 7814 r1pwss 8255 dfac5lem4 8557 climuni 13616 rlimno1 13717 caurcvg2 13744 sscfn1 15722 gsumval2a 16522 gsumval3 17541 opnnei 20136 dislly 20512 lfinpfin 20539 txcmplem1 20656 ufileu 20934 alexsubALT 21066 metustel 21565 metustfbas 21572 i1faddlem 22651 ulmval 23335 brbtwn 24929 wwlknredwwlkn0 25455 iseupa 25693 numclwwlkun 25807 iccllyscon 29973 cvmopnlem 30001 cvmlift2lem10 30035 cvmlift3lem8 30049 sdclem2 32071 heibor1lem 32141 elrfi 35536 eldiophb 35599 dnnumch2 35903 vtxduhgr0nedg 39546 |
Copyright terms: Public domain | W3C validator |