![]() |
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 2336 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfcv 2336 |
. 2
![]() ![]() ![]() ![]() | |
3 | 1, 2 | raleqf 2686 |
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 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2175 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ral 2477 |
This theorem is referenced by: raleqi 2694 raleqdv 2696 raleqbi1dv 2702 sbralie 2744 inteq 3873 iineq1 3926 bnd2 4202 frforeq2 4376 weeq2 4388 ordeq 4403 reg2exmid 4568 reg3exmid 4612 omsinds 4654 fncnv 5320 funimaexglem 5337 isoeq4 5847 acexmidlemv 5916 tfrlem1 6361 tfr0dm 6375 tfrlemisucaccv 6378 tfrlemi1 6385 tfrlemi14d 6386 tfrexlem 6387 tfr1onlemsucaccv 6394 tfr1onlemaccex 6401 tfr1onlemres 6402 tfrcllemsucaccv 6407 tfrcllembxssdm 6409 tfrcllemaccex 6414 tfrcllemres 6415 tfrcldm 6416 ixpeq1 6763 ac6sfi 6954 fimax2gtri 6957 dcfi 7040 supeq1 7045 supeq2 7048 nnnninfeq2 7188 isomni 7195 ismkv 7212 iswomni 7224 tapeq2 7313 sup3exmid 8976 rexanuz 11132 rexfiuz 11133 fimaxre2 11370 modfsummod 11601 mhmpropd 13038 isghm 13313 iscmn 13363 srgideu 13468 dfrhm2 13650 cnprcl2k 14374 ispsmet 14491 ismet 14512 isxmet 14513 cncfval 14727 dvcn 14849 setindis 15459 bdsetindis 15461 strcoll2 15475 strcollnfALT 15478 |
Copyright terms: Public domain | W3C validator |