![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralbidv2 | Structured version Visualization version Unicode version |
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Apr-1997.) |
Ref | Expression |
---|---|
ralbidv2.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ralbidv2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbidv2.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | albidv 1766 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-ral 2741 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-ral 2741 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3bitr4g 292 |
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 1668 ax-4 1681 ax-5 1757 |
This theorem depends on definitions: df-bi 189 df-ral 2741 |
This theorem is referenced by: ralbidva 2823 ralss 3494 oneqmini 5473 ordunisuc2 6668 dfsmo2 7063 wemapsolem 8062 zorn2lem1 8923 raluz 11204 limsupgle 13528 ello12 13573 elo12 13584 lo1resb 13621 rlimresb 13622 o1resb 13623 isprm3 14626 ist1 20330 ist1-2 20356 hausdiag 20653 xkopt 20663 cnflf 21010 cnfcf 21050 metcnp 21549 caucfil 22246 mdegleb 23006 eulerpartlemgvv 29202 filnetlem4 31030 isprm7 36654 hoidmvle 38416 elbigo2 40350 |
Copyright terms: Public domain | W3C validator |