![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ralbidv | Unicode version |
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.) |
Ref | Expression |
---|---|
ralbidv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ralbidv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1418 |
. 2
![]() ![]() ![]() ![]() | |
2 | ralbidv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ralbid 2318 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-4 1397 ax-17 1416 |
This theorem depends on definitions: df-bi 110 df-nf 1347 df-ral 2305 |
This theorem is referenced by: ralbii 2324 2ralbidv 2342 rexralbidv 2344 r19.32vdc 2453 raleqbi1dv 2507 raleqbidv 2511 cbvral2v 2535 rspc2 2655 rspc3v 2659 reu6i 2726 reu7 2730 sbcralt 2828 sbcralg 2830 raaanlem 3320 r19.12sn 3427 2ralunsn 3560 elintg 3614 elintrabg 3619 eliin 3653 bnd2 3917 poeq1 4027 soeq1 4043 reusv3 4158 posng 4355 ralxpf 4425 cnvpom 4803 funcnvuni 4911 dff4im 5256 dff13f 5352 eusvobj2 5441 ofreq 5657 smoeq 5846 recseq 5862 tfr0 5878 tfrlemiex 5886 elinp 6457 prloc 6474 cauappcvgprlemladdru 6628 cauappcvgprlemladdrl 6629 caucvgpr 6653 nnsub 7733 indstr 8312 ublbneg 8324 lbzbi 8327 iccsupr 8605 bj-omtrans 9416 |
Copyright terms: Public domain | W3C validator |