Metamath Proof Explorer
Description: Weaker version of rexlimiv . (Contributed by FL, 19-Sep-2011)
(Proof shortened by Wolf Lammen, 23-Dec-2024)
|
|
Ref |
Expression |
|
Hypothesis |
rexlimivw.1 |
|
|
Assertion |
rexlimivw |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
rexlimivw.1 |
|
2 |
1
|
adantl |
|
3 |
2
|
rexlimiva |
|