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 2312 | . 2 | |
2 | nfcv 2312 | . 2 | |
3 | 1, 2 | raleqf 2661 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wceq 1348 wral 2448 |
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 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-sb 1756 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 |
This theorem is referenced by: raleqi 2669 raleqdv 2671 raleqbi1dv 2673 sbralie 2714 inteq 3832 iineq1 3885 bnd2 4157 frforeq2 4328 weeq2 4340 ordeq 4355 reg2exmid 4518 reg3exmid 4562 omsinds 4604 fncnv 5262 funimaexglem 5279 isoeq4 5781 acexmidlemv 5849 tfrlem1 6285 tfr0dm 6299 tfrlemisucaccv 6302 tfrlemi1 6309 tfrlemi14d 6310 tfrexlem 6311 tfr1onlemsucaccv 6318 tfr1onlemaccex 6325 tfr1onlemres 6326 tfrcllemsucaccv 6331 tfrcllembxssdm 6333 tfrcllemaccex 6338 tfrcllemres 6339 tfrcldm 6340 ixpeq1 6684 ac6sfi 6873 fimax2gtri 6876 dcfi 6955 supeq1 6960 supeq2 6963 nnnninfeq2 7102 isomni 7109 ismkv 7126 iswomni 7138 sup3exmid 8862 rexanuz 10941 rexfiuz 10942 fimaxre2 11179 modfsummod 11410 mhmpropd 12678 cnprcl2k 12961 ispsmet 13078 ismet 13099 isxmet 13100 cncfval 13314 dvcn 13419 setindis 13964 bdsetindis 13966 strcoll2 13980 strcollnfALT 13983 |
Copyright terms: Public domain | W3C validator |