![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2rexbidv | Unicode version |
Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) |
Ref | Expression |
---|---|
2ralbidv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
2rexbidv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | rexbidv 2392 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | rexbidv 2392 |
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 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-4 1452 ax-17 1471 ax-ial 1479 |
This theorem depends on definitions: df-bi 116 df-nf 1402 df-rex 2376 |
This theorem is referenced by: f1oiso 5643 elrnmpt2g 5795 elrnmpt2 5796 ralrnmpt2 5797 rexrnmpt2 5798 ovelrn 5831 eroveu 6423 genipv 7165 genpelxp 7167 genpelvl 7168 genpelvu 7169 axcnre 7513 apreap 8161 apreim 8177 bezoutlemnewy 11412 bezoutlema 11415 bezoutlemb 11416 |
Copyright terms: Public domain | W3C validator |