New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > rexlimdvva | Unicode version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.) |
Ref | Expression |
---|---|
rexlimdvva.1 |
Ref | Expression |
---|---|
rexlimdvva |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimdvva.1 | . . 3 | |
2 | 1 | ex 423 | . 2 |
3 | 2 | rexlimdvv 2744 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 358 wcel 1710 wrex 2615 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-11 1746 |
This theorem depends on definitions: df-bi 177 df-an 360 df-ex 1542 df-nf 1545 df-ral 2619 df-rex 2620 |
This theorem is referenced by: nnsucelr 4428 nndisjeq 4429 prepeano4 4451 ltfintr 4459 ncfinlower 4483 tfindi 4496 tfinsuc 4498 nnadjoin 4520 nnpweq 4523 sfindbl 4530 tfinnn 4534 vfinspsslem1 4550 ncdisjun 6136 peano4nc 6150 ncspw1eu 6159 ce0addcnnul 6179 sbth 6206 dflec2 6210 lectr 6211 |
Copyright terms: Public domain | W3C validator |