![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > raleq | Unicode version |
Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) |
Ref | Expression |
---|---|
raleq |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2282 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfcv 2282 |
. 2
![]() ![]() ![]() ![]() | |
3 | 1, 2 | raleqf 2625 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
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-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-cleq 2133 df-clel 2136 df-nfc 2271 df-ral 2422 |
This theorem is referenced by: raleqi 2633 raleqdv 2635 raleqbi1dv 2637 sbralie 2673 inteq 3782 iineq1 3835 bnd2 4105 frforeq2 4275 weeq2 4287 ordeq 4302 reg2exmid 4459 reg3exmid 4502 omsinds 4543 fncnv 5197 funimaexglem 5214 isoeq4 5713 acexmidlemv 5780 tfrlem1 6213 tfr0dm 6227 tfrlemisucaccv 6230 tfrlemi1 6237 tfrlemi14d 6238 tfrexlem 6239 tfr1onlemsucaccv 6246 tfr1onlemaccex 6253 tfr1onlemres 6254 tfrcllemsucaccv 6259 tfrcllembxssdm 6261 tfrcllemaccex 6266 tfrcllemres 6267 tfrcldm 6268 ixpeq1 6611 ac6sfi 6800 fimax2gtri 6803 supeq1 6881 supeq2 6884 isomni 7016 ismkv 7035 iswomni 7047 sup3exmid 8739 rexanuz 10792 rexfiuz 10793 fimaxre2 11030 modfsummod 11259 cnprcl2k 12414 ispsmet 12531 ismet 12552 isxmet 12553 cncfval 12767 dvcn 12872 setindis 13336 bdsetindis 13338 strcoll2 13352 strcollnfALT 13355 |
Copyright terms: Public domain | W3C validator |