Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rexralbidv | Unicode version |
Description: Formula-building rule for restricted quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) |
Ref | Expression |
---|---|
2ralbidv.1 |
Ref | Expression |
---|---|
rexralbidv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidv.1 | . . 3 | |
2 | 1 | ralbidv 2464 | . 2 |
3 | 2 | rexbidv 2465 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wral 2442 wrex 2443 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-4 1497 ax-17 1513 ax-ial 1521 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-ral 2447 df-rex 2448 |
This theorem is referenced by: caucvgpr 7614 caucvgprpr 7644 caucvgsrlemgt1 7727 caucvgsrlemoffres 7732 axcaucvglemres 7831 cvg1nlemres 10913 rexfiuz 10917 resqrexlemgt0 10948 resqrexlemoverl 10949 resqrexlemglsq 10950 resqrexlemsqa 10952 resqrexlemex 10953 cau3lem 11042 caubnd2 11045 climi 11214 2clim 11228 ennnfonelemim 12300 lmcvg 12764 lmss 12793 txlm 12826 metcnpi 13062 metcnpi2 13063 elcncf 13107 cncfi 13112 limcimo 13181 cnplimclemr 13185 limccoap 13194 |
Copyright terms: Public domain | W3C validator |