![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reximdai | Structured version Visualization version Unicode version |
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.) |
Ref | Expression |
---|---|
reximdai.1 |
![]() ![]() ![]() ![]() |
reximdai.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
reximdai |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximdai.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | reximdai.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ralrimi 2788 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | rexim 2852 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | syl 17 |
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-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: reximdvaiOLD 2860 tz7.49 7162 hsmexlem2 8857 acunirnmpt2 28262 acunirnmpt2f 28263 locfinreflem 28667 cmpcref 28677 indexdom 32061 filbcmb 32067 cdlemefr29exN 33969 disjrnmpt2 37463 fompt 37467 disjinfi 37468 supxrge 37561 suplesup 37562 infrglbOLD 37669 limsupre 37721 limsupreOLD 37722 stoweidlem31 37892 stoweidlem34 37895 fourierdlem73 38043 sge0pnffigt 38238 sge0ltfirp 38242 iundjiun 38298 ovnlerp 38384 2reurex 38602 |
Copyright terms: Public domain | W3C validator |