Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > raleqdv | Unicode version |
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.) |
Ref | Expression |
---|---|
raleq1d.1 |
Ref | Expression |
---|---|
raleqdv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleq1d.1 | . 2 | |
2 | raleq 2626 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wceq 1331 wral 2416 |
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 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ral 2421 |
This theorem is referenced by: raleqbidv 2638 raleqbidva 2640 omsinds 4535 cbvfo 5686 isoselem 5721 ofrfval 5990 issmo2 6186 smoeq 6187 tfrlemisucaccv 6222 tfr1onlemsucaccv 6238 tfrcllemsucaccv 6251 fzrevral2 9886 fzrevral3 9887 fzshftral 9888 fzoshftral 10015 uzsinds 10215 iseqf1olemqk 10267 seq3f1olemstep 10274 seq3f1olemp 10275 caucvgre 10753 cvg1nlemres 10757 rexuz3 10762 resqrexlemoverl 10793 resqrexlemsqa 10796 resqrexlemex 10797 climconst 11059 climshftlemg 11071 serf0 11121 summodclem2 11151 summodc 11152 zsumdc 11153 mertenslemi1 11304 prodmodclem2 11346 prodmodc 11347 zsupcllemstep 11638 zsupcllemex 11639 infssuzex 11642 prmind2 11801 ennnfoneleminc 11924 ennnfonelemex 11927 ennnfonelemnn0 11935 ennnfonelemr 11936 lmfval 12361 lmconst 12385 cncnp 12399 metss 12663 sin0pilem2 12863 nninfsellemdc 13206 nninfself 13209 nninfsellemeqinf 13212 nninfomni 13215 |
Copyright terms: Public domain | W3C validator |