![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > r19.23v | Structured version Visualization version Unicode version |
Description: Restricted quantifier version of 19.23v 1829. Version of r19.23 2878 with a dv condition. (Contributed by NM, 31-Aug-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.) |
Ref | Expression |
---|---|
r19.23v |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con34b 298 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ralbii 2831 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | r19.21v 2805 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | dfrex2 2850 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | imbi1i 331 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | con1b 339 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | bitr2i 258 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 2, 3, 7 | 3bitri 279 |
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 1680 ax-4 1693 ax-5 1769 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ex 1675 df-ral 2754 df-rex 2755 |
This theorem is referenced by: rexlimiv 2885 ralxpxfr2d 3176 uniiunlem 3529 dfiin2g 4325 iunss 4333 ralxfr2d 4630 ssrel2 4944 reliun 4973 funimass4 5939 ralrnmpt2 6438 kmlem12 8617 fimaxre3 10581 gcdcllem1 14522 vdwmc2 14978 iunocv 19293 islindf4 19445 ovolgelb 22482 dyadmax 22605 itg2leub 22741 mptelee 24974 nmoubi 26462 nmopub 27610 nmfnleub 27627 sigaclcu2 28991 untuni 30385 dfpo2 30444 heibor1lem 32186 ispsubsp2 33356 pmapglbx 33379 2reu4a 38648 |
Copyright terms: Public domain | W3C validator |